/[mojave]/metaprl/editor/ml/mp.ml
ViewVC logotype

Diff of /metaprl/editor/ml/mp.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 2753 by jyh, Fri Jun 25 00:19:15 1999 UTC revision 2775 by jyh, Sun Jul 4 13:13:44 1999 UTC
# Line 57  Line 57 
57  let create_pkg = create_pkg (get_current_shell ())  let create_pkg = create_pkg (get_current_shell ())
58  let set_writeable () = set_writeable (get_current_shell ())  let set_writeable () = set_writeable (get_current_shell ())
59  let save () = save (get_current_shell ())  let save () = save (get_current_shell ())
60    let export () = export (get_current_shell ())
61  let save_all () = save_all (get_current_shell ())  let save_all () = save_all (get_current_shell ())
62    
63  (*  (*
# Line 108  Line 109 
109  let unfold () = unfold (get_current_shell ())  let unfold () = unfold (get_current_shell ())
110  let copy s = copy (get_current_shell ()) s  let copy s = copy (get_current_shell ()) s
111  let paste s = paste (get_current_shell ()) s  let paste s = paste (get_current_shell ()) s
112    let kreitz () = kreitz (get_current_shell ())
113    let clean () = clean (get_current_shell ())
114    let squash () = squash (get_current_shell ())
115  let make_assum () = make_assum (get_current_shell ())  let make_assum () = make_assum (get_current_shell ())
116    
117  (*  (*
# Line 134  Line 138 
138  let edit_save = edit_save (get_current_shell ())  let edit_save = edit_save (get_current_shell ())
139  let edit_undo () = edit_undo (get_current_shell ())  let edit_undo () = edit_undo (get_current_shell ())
140    
141    let shell_get_term = Shell_state.ShellState.get_term
142    
143  let _ = ShellHTTP.main ()  let _ = ShellHTTP.main ()
144    
145  (*  (*

Legend:
Removed from v.2753  
changed lines
  Added in v.2775

  ViewVC Help
Powered by ViewVC 1.1.26