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

Annotation of /metaprl/editor/ml/mp.ml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2922 - (hide 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 jyh 2494 (*
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 jyh 2743 module Shell = Shell.Shell (Shell_p4.ShellP4 (Shell_state.ShellState))
34     module ShellHTTP = Shell_http.ShellHTTP (Shell)
35 jyh 2494
36     open Shell
37    
38 lolorigo 2922 module Nuprl = Nuprl_eval.Nuprl
39     module NuprlRun = Nuprl_run.NuprlRun
40    
41     let run_nuprl = NuprlRun.run_connection
42    
43 jyh 2494 (*
44 jyh 2743 * 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 jyh 2494 * Navigation and display.
53     *)
54 jyh 2743 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 jyh 2494
58     (*
59     * Module commands.
60     *)
61 jyh 2743 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 jyh 2775 let export () = export (get_current_shell ())
66 jyh 2743 let save_all () = save_all (get_current_shell ())
67 jyh 2494
68     (*
69     * The possible objects in a package.
70     *)
71 jyh 2743 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 jyh 2494
85     (*
86     * View, close, check object.
87     * An object is not installed until it is checked.
88     *)
89 jyh 2743 let view = view (get_current_shell ())
90 jyh 2753 let ls s = ls (get_current_shell ()) s
91 jyh 2494
92     (*
93     * Editing commands.
94     *)
95 jyh 2743 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 jyh 2494
103     (*
104     * Proof editing.
105     *)
106 jyh 2743 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 jyh 2753 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 jyh 2775 let kreitz () = kreitz (get_current_shell ())
118     let clean () = clean (get_current_shell ())
119     let squash () = squash (get_current_shell ())
120 jyh 2753 let make_assum () = make_assum (get_current_shell ())
121 jyh 2494
122     (*
123     * Nuprl5 interface.
124     *)
125 jyh 2743 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 jyh 2494
146 jyh 2775 let shell_get_term = Shell_state.ShellState.get_term
147    
148 jyh 2743 let _ = ShellHTTP.main ()
149 jyh 2494
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