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

Contents of /metaprl/editor/ml/mp.ml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2922 - (show annotations) (download)
Thu Mar 16 19:52:02 2000 UTC (21 years, 4 months ago) by lolorigo
File size: 5505 byte(s)
added/improved functionality for metaprl/jprover/nuprl5 io

1 (*
2 * This is the main file for MetaPRL.
3 *
4 * ----------------------------------------------------------------
5 *
6 * This file is part of MetaPRL, a modular, higher order
7 * logical framework that provides a logical programming
8 * environment for OCaml and other languages.
9 *
10 * See the file doc/index.html for information on Nuprl,
11 * OCaml, and more information about this system.
12 *
13 * Copyright (C) 1998 Jason Hickey, Cornell University
14 *
15 * This program is free software; you can redistribute it and/or
16 * modify it under the terms of the GNU General Public License
17 * as published by the Free Software Foundation; either version 2
18 * of the License, or (at your option) any later version.
19 *
20 * This program is distributed in the hope that it will be useful,
21 * but WITHOUT ANY WARRANTY; without even the implied warranty of
22 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
23 * GNU General Public License for more details.
24 *
25 * You should have received a copy of the GNU General Public License
26 * along with this program; if not, write to the Free Software
27 * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
28 *
29 * Author: Jason Hickey
30 * jyh@cs.cornell.edu
31 *)
32
33 module Shell = Shell.Shell (Shell_p4.ShellP4 (Shell_state.ShellState))
34 module ShellHTTP = Shell_http.ShellHTTP (Shell)
35
36 open Shell
37
38 module Nuprl = Nuprl_eval.Nuprl
39 module NuprlRun = Nuprl_run.NuprlRun
40
41 let run_nuprl = NuprlRun.run_connection
42
43 (*
44 * Job control.
45 *)
46 let fork = fork (get_current_shell ())
47 let pid = pid (get_current_shell ())
48 let jobs = jobs (get_current_shell ())
49 let fg = fg (get_current_shell ())
50
51 (*
52 * Navigation and display.
53 *)
54 let cd = cd (get_current_shell ())
55 let pwd () = pwd (get_current_shell ())
56 let set_window_width = set_window_width (get_current_shell ())
57
58 (*
59 * Module commands.
60 *)
61 let load = load (get_current_shell ())
62 let create_pkg = create_pkg (get_current_shell ())
63 let set_writeable () = set_writeable (get_current_shell ())
64 let save () = save (get_current_shell ())
65 let export () = export (get_current_shell ())
66 let save_all () = save_all (get_current_shell ())
67
68 (*
69 * The possible objects in a package.
70 *)
71 let create_rw = create_rw (get_current_shell ())
72 let create_axiom = create_axiom (get_current_shell ())
73 let create_thm = create_thm (get_current_shell ())
74 let create_tptp = create_tptp (get_current_shell ())
75 let create_opname = create_opname (get_current_shell ())
76 let create_condition = create_condition (get_current_shell ())
77 let create_parent = create_parent (get_current_shell ())
78 let create_dform = create_dform (get_current_shell ())
79 let create_prec = create_prec (get_current_shell ())
80 let create_prec_rel = create_prec_rel (get_current_shell ())
81 let create_resource = create_resource (get_current_shell ())
82 let create_infix = create_infix (get_current_shell ())
83 let create_ml = create_ml (get_current_shell ())
84
85 (*
86 * View, close, check object.
87 * An object is not installed until it is checked.
88 *)
89 let view = view (get_current_shell ())
90 let ls s = ls (get_current_shell ()) s
91
92 (*
93 * Editing commands.
94 *)
95 let set_goal = set_goal (get_current_shell ())
96 let set_redex = set_redex (get_current_shell ())
97 let set_contractum = set_contractum (get_current_shell ())
98 let set_assumptions = set_assumptions (get_current_shell ())
99 let set_params = set_params (get_current_shell ())
100 let check () = check (get_current_shell ())
101 let expand () = expand (get_current_shell ())
102
103 (*
104 * Proof editing.
105 *)
106 let root () = root (get_current_shell ())
107 let up = up (get_current_shell ())
108 let down = down (get_current_shell ())
109 let goal () = goal (get_current_shell ())
110 let refine = refine (get_current_shell ())
111 let undo () = undo (get_current_shell ())
112 let redo () = redo (get_current_shell ())
113 let nop () = nop (get_current_shell ())
114 let unfold () = unfold (get_current_shell ())
115 let copy s = copy (get_current_shell ()) s
116 let paste s = paste (get_current_shell ()) s
117 let kreitz () = kreitz (get_current_shell ())
118 let clean () = clean (get_current_shell ())
119 let squash () = squash (get_current_shell ())
120 let make_assum () = make_assum (get_current_shell ())
121
122 (*
123 * Nuprl5 interface.
124 *)
125 let edit_list_modules () = edit_list_modules (get_current_shell ())
126 let edit_list_module_all = edit_list_module_all (get_current_shell ())
127 let edit_list_module = edit_list_module (get_current_shell ())
128 let edit_list_module_rw = edit_list_module_rw (get_current_shell ())
129 let edit_list_parents = edit_list_parents (get_current_shell ())
130 let edit_list_dforms = edit_list_dforms (get_current_shell ())
131 let edit_list_precs = edit_list_precs (get_current_shell ())
132 let edit_list_prec_rels = edit_list_prec_rels (get_current_shell ())
133 let edit_create_thm = edit_create_thm (get_current_shell ())
134 let edit_create_rw = edit_create_rw (get_current_shell ())
135 let edit_cd_thm = edit_cd_thm (get_current_shell ())
136 let edit_set_goal = edit_set_goal (get_current_shell ())
137 let edit_set_redex = edit_set_redex (get_current_shell ())
138 let edit_set_contractum = edit_set_contractum (get_current_shell ())
139 let edit_set_assumptions = edit_set_assumptions (get_current_shell ())
140 let edit_set_params = edit_set_params (get_current_shell ())
141 let edit_refine = edit_refine (get_current_shell ())
142 let edit_node = edit_node (get_current_shell ())
143 let edit_save = edit_save (get_current_shell ())
144 let edit_undo () = edit_undo (get_current_shell ())
145
146 let shell_get_term = Shell_state.ShellState.get_term
147
148 let _ = ShellHTTP.main ()
149
150 (*
151 * -*-
152 * Local Variables:
153 * Caml-master: "refiner"
154 * End:
155 * -*-
156 *)

Properties

Name Value
svn:eol-style native
svn:keywords Author Date Id Revision

  ViewVC Help
Powered by ViewVC 1.1.26