/[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 2743 by jyh, Wed Jun 23 04:50:29 1999 UTC revision 2753 by jyh, Fri Jun 25 00:19:15 1999 UTC
# Line 81  Line 81 
81   * An object is not installed until it is checked.   * An object is not installed until it is checked.
82   *)   *)
83  let view = view (get_current_shell ())  let view = view (get_current_shell ())
84  let ls () = ls (get_current_shell ())  let ls s = ls (get_current_shell ()) s
85    
86  (*  (*
87   * Editing commands.   * Editing commands.
# Line 103  Line 103 
103  let goal () = goal (get_current_shell ())  let goal () = goal (get_current_shell ())
104  let refine = refine (get_current_shell ())  let refine = refine (get_current_shell ())
105  let undo () = undo (get_current_shell ())  let undo () = undo (get_current_shell ())
106    let redo () = redo (get_current_shell ())
107    let nop () = nop (get_current_shell ())
108    let unfold () = unfold (get_current_shell ())
109    let copy s = copy (get_current_shell ()) s
110    let paste s = paste (get_current_shell ()) s
111    let make_assum () = make_assum (get_current_shell ())
112    
113  (*  (*
114   * Nuprl5 interface.   * Nuprl5 interface.

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

  ViewVC Help
Powered by ViewVC 1.1.26