/[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 2604 by lolorigo, Thu Mar 4 15:02:04 1999 UTC revision 2743 by jyh, Wed Jun 23 04:50:29 1999 UTC
# Line 30  Line 30 
30   * jyh@cs.cornell.edu   * jyh@cs.cornell.edu
31   *)   *)
32    
33  module Shell = Shell.Shell (Shell_p4.ShellP4)  module Shell = Shell.Shell (Shell_p4.ShellP4 (Shell_state.ShellState))
34    module ShellHTTP = Shell_http.ShellHTTP (Shell)
35    
36  open Shell  open Shell
37    
38  (*  (*
39     * Job control.
40     *)
41    let fork = fork (get_current_shell ())
42    let pid = pid (get_current_shell ())
43    let jobs = jobs (get_current_shell ())
44    let fg = fg (get_current_shell ())
45    
46    (*
47   * Navigation and display.   * Navigation and display.
48   *)   *)
49  let cd = cd  let cd = cd (get_current_shell ())
50  let pwd = pwd  let pwd () = pwd (get_current_shell ())
51  let set_window_width = set_window_width  let set_window_width = set_window_width (get_current_shell ())
52    
53  (*  (*
54   * Module commands.   * Module commands.
55   *)   *)
56  let load = load  let load = load (get_current_shell ())
57  let create_pkg = create_pkg  let create_pkg = create_pkg (get_current_shell ())
58  let set_writeable = set_writeable  let set_writeable () = set_writeable (get_current_shell ())
59  let save = save  let save () = save (get_current_shell ())
60  let save_all = save_all  let save_all () = save_all (get_current_shell ())
61    
62  (*  (*
63   * The possible objects in a package.   * The possible objects in a package.
64   *)   *)
65  let create_rw = create_rw  let create_rw = create_rw (get_current_shell ())
66  let create_axiom = create_axiom  let create_axiom = create_axiom (get_current_shell ())
67  let create_thm = create_thm  let create_thm = create_thm (get_current_shell ())
68  let create_tptp = create_tptp  let create_tptp = create_tptp (get_current_shell ())
69  let create_opname = create_opname  let create_opname = create_opname (get_current_shell ())
70  let create_condition = create_condition  let create_condition = create_condition (get_current_shell ())
71  let create_parent = create_parent  let create_parent = create_parent (get_current_shell ())
72  let create_dform = create_dform  let create_dform = create_dform (get_current_shell ())
73  let create_prec = create_prec  let create_prec = create_prec (get_current_shell ())
74  let create_prec_rel = create_prec_rel  let create_prec_rel = create_prec_rel (get_current_shell ())
75  let create_resource = create_resource  let create_resource = create_resource (get_current_shell ())
76  let create_infix = create_infix  let create_infix = create_infix (get_current_shell ())
77  let create_ml = create_ml  let create_ml = create_ml (get_current_shell ())
78    
79  (*  (*
80   * View, close, check object.   * View, close, check object.
81   * An object is not installed until it is checked.   * An object is not installed until it is checked.
82   *)   *)
83  let view = view  let view = view (get_current_shell ())
84  let ls = ls  let ls () = ls (get_current_shell ())
85    
86  (*  (*
87   * Editing commands.   * Editing commands.
88   *)   *)
89  let set_goal = set_goal  let set_goal = set_goal (get_current_shell ())
90  let set_redex = set_redex  let set_redex = set_redex (get_current_shell ())
91  let set_contractum = set_contractum  let set_contractum = set_contractum (get_current_shell ())
92  let set_assumptions = set_assumptions  let set_assumptions = set_assumptions (get_current_shell ())
93  let set_params = set_params  let set_params = set_params (get_current_shell ())
94  let check = check  let check () = check (get_current_shell ())
95  let expand = expand  let expand () = expand (get_current_shell ())
96    
97  (*  (*
98   * Proof editing.   * Proof editing.
99   *)   *)
100  let root = root  let root () = root (get_current_shell ())
101  let up = up  let up = up (get_current_shell ())
102  let down = down  let down = down (get_current_shell ())
103  let goal = goal  let goal () = goal (get_current_shell ())
104  let refine = refine  let refine = refine (get_current_shell ())
105  let undo = undo  let undo () = undo (get_current_shell ())
 let fold = fold  
 let fold_all = fold_all  
106    
107  (*  (*
108   * Nuprl5 interface.   * Nuprl5 interface.
109   *)   *)
110  let edit_list_modules = edit_list_modules  let edit_list_modules () = edit_list_modules (get_current_shell ())
111  let edit_list_module_all = edit_list_module_all  let edit_list_module_all = edit_list_module_all (get_current_shell ())
112  let edit_list_module = edit_list_module  let edit_list_module = edit_list_module (get_current_shell ())
113  let edit_list_module_rw = edit_list_module_rw  let edit_list_module_rw = edit_list_module_rw (get_current_shell ())
114  let edit_list_parents = edit_list_parents  let edit_list_parents = edit_list_parents (get_current_shell ())
115  let edit_list_dforms = edit_list_dforms  let edit_list_dforms = edit_list_dforms (get_current_shell ())
116  let edit_list_precs = edit_list_precs  let edit_list_precs = edit_list_precs (get_current_shell ())
117  let edit_list_prec_rels = edit_list_prec_rels  let edit_list_prec_rels = edit_list_prec_rels (get_current_shell ())
118  let edit_create_thm = edit_create_thm  let edit_create_thm = edit_create_thm (get_current_shell ())
119  let edit_create_rw = edit_create_rw  let edit_create_rw = edit_create_rw (get_current_shell ())
120  let edit_cd_thm = edit_cd_thm  let edit_cd_thm = edit_cd_thm (get_current_shell ())
121  let edit_set_goal = edit_set_goal  let edit_set_goal = edit_set_goal (get_current_shell ())
122  let edit_set_redex = edit_set_redex  let edit_set_redex = edit_set_redex (get_current_shell ())
123  let edit_set_contractum = edit_set_contractum  let edit_set_contractum = edit_set_contractum (get_current_shell ())
124  let edit_set_assumptions = edit_set_assumptions  let edit_set_assumptions = edit_set_assumptions (get_current_shell ())
125  let edit_set_params = edit_set_params  let edit_set_params = edit_set_params (get_current_shell ())
126  let edit_refine = edit_refine  let edit_refine = edit_refine (get_current_shell ())
127  let edit_node = edit_node  let edit_node = edit_node (get_current_shell ())
128  let edit_save = edit_save  let edit_save = edit_save (get_current_shell ())
129  let edit_undo = edit_undo  let edit_undo () = edit_undo (get_current_shell ())
130    
131  let _ = Shell.main ()  let _ = ShellHTTP.main ()
132    
133  (*  (*
134   * -*-   * -*-

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

  ViewVC Help
Powered by ViewVC 1.1.26