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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2775 - (hide annotations) (download)
Sun Jul 4 13:13:44 1999 UTC (22 years ago) by jyh
File size: 5392 byte(s)
Things seem to be working pretty smoothly now.  This is mostly minor
fixes.  Still need to fix the problems with the mp toploop.

    1. Proofs now use Alexey's ASCII format.  By default, proofs
       should be saved to CVS in .prla format.  You can generate ASCII
       files by using "make export", or you can use the "export ()"
       instead of the "save ()" command in the editor.  For speed,
       .prlb files are now saved in a raw, marshaled format.  When you
       edit a theory, the newest of .cmoz, .prlb, or .prla files is
       loaded.  There is a new command "convert" to convert between
       all the different proof file formats.
          convert -I ... [-raw|-term|-lib|-ascii] -impl file.cmoz
          raw: save the file in fast, raw format
	  term: save the file as <magic#>/<marshaled term_io>
	  lib: send the file to the Nuprl5 library
	  ascii: create a .prla file

       Developers: _please_ mention any changes to the basic data
          structures in your CVS logs.  The things that matter are:
          Refiner.Refiner.TermType.term
	  Filter_summary.summary_info
	  Tactic_boot_sig.TacticType.{tactic_arg,extract}
	  Proof_boot.io_proof

       Users: to be safe, save all your proofs using "make export"
          before doing a cvs update.

    2. "expand ()" and "expand_all ()" now work.  I also added
       "clean ()" and "clean_all ()" commands to remove those peasky
       dangling proof nodes when you are satisfied with a proof.  By
       default, proofs are saved only down to the innermost rule-box
       level, and primitive refinements are omitted.  I haven't added
       a "deep_save ()" command; it seems unecessary.

    3. Sorry, but I had to move theories/boot into the filter.  There
       are no major changes here, but the directory structure in
       filter has changed significantly.

    4. I added a THEORIES variable to the mk/config file that
       specifies what theories you want to compile.  This means that
       you don't have to edit all the Makefiles when you add a theory,
       and it also means that you can keep your own theories without
       having to commit them to cvs.

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     (*
39 jyh 2743 * 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 jyh 2494 * Navigation and display.
48     *)
49 jyh 2743 let cd = cd (get_current_shell ())
50     let pwd () = pwd (get_current_shell ())
51     let set_window_width = set_window_width (get_current_shell ())
52 jyh 2494
53     (*
54     * Module commands.
55     *)
56 jyh 2743 let load = load (get_current_shell ())
57     let create_pkg = create_pkg (get_current_shell ())
58     let set_writeable () = set_writeable (get_current_shell ())
59     let save () = save (get_current_shell ())
60 jyh 2775 let export () = export (get_current_shell ())
61 jyh 2743 let save_all () = save_all (get_current_shell ())
62 jyh 2494
63     (*
64     * The possible objects in a package.
65     *)
66 jyh 2743 let create_rw = create_rw (get_current_shell ())
67     let create_axiom = create_axiom (get_current_shell ())
68     let create_thm = create_thm (get_current_shell ())
69     let create_tptp = create_tptp (get_current_shell ())
70     let create_opname = create_opname (get_current_shell ())
71     let create_condition = create_condition (get_current_shell ())
72     let create_parent = create_parent (get_current_shell ())
73     let create_dform = create_dform (get_current_shell ())
74     let create_prec = create_prec (get_current_shell ())
75     let create_prec_rel = create_prec_rel (get_current_shell ())
76     let create_resource = create_resource (get_current_shell ())
77     let create_infix = create_infix (get_current_shell ())
78     let create_ml = create_ml (get_current_shell ())
79 jyh 2494
80     (*
81     * View, close, check object.
82     * An object is not installed until it is checked.
83     *)
84 jyh 2743 let view = view (get_current_shell ())
85 jyh 2753 let ls s = ls (get_current_shell ()) s
86 jyh 2494
87     (*
88     * Editing commands.
89     *)
90 jyh 2743 let set_goal = set_goal (get_current_shell ())
91     let set_redex = set_redex (get_current_shell ())
92     let set_contractum = set_contractum (get_current_shell ())
93     let set_assumptions = set_assumptions (get_current_shell ())
94     let set_params = set_params (get_current_shell ())
95     let check () = check (get_current_shell ())
96     let expand () = expand (get_current_shell ())
97 jyh 2494
98     (*
99     * Proof editing.
100     *)
101 jyh 2743 let root () = root (get_current_shell ())
102     let up = up (get_current_shell ())
103     let down = down (get_current_shell ())
104     let goal () = goal (get_current_shell ())
105     let refine = refine (get_current_shell ())
106     let undo () = undo (get_current_shell ())
107 jyh 2753 let redo () = redo (get_current_shell ())
108     let nop () = nop (get_current_shell ())
109     let unfold () = unfold (get_current_shell ())
110     let copy s = copy (get_current_shell ()) s
111     let paste s = paste (get_current_shell ()) s
112 jyh 2775 let kreitz () = kreitz (get_current_shell ())
113     let clean () = clean (get_current_shell ())
114     let squash () = squash (get_current_shell ())
115 jyh 2753 let make_assum () = make_assum (get_current_shell ())
116 jyh 2494
117     (*
118     * Nuprl5 interface.
119     *)
120 jyh 2743 let edit_list_modules () = edit_list_modules (get_current_shell ())
121     let edit_list_module_all = edit_list_module_all (get_current_shell ())
122     let edit_list_module = edit_list_module (get_current_shell ())
123     let edit_list_module_rw = edit_list_module_rw (get_current_shell ())
124     let edit_list_parents = edit_list_parents (get_current_shell ())
125     let edit_list_dforms = edit_list_dforms (get_current_shell ())
126     let edit_list_precs = edit_list_precs (get_current_shell ())
127     let edit_list_prec_rels = edit_list_prec_rels (get_current_shell ())
128     let edit_create_thm = edit_create_thm (get_current_shell ())
129     let edit_create_rw = edit_create_rw (get_current_shell ())
130     let edit_cd_thm = edit_cd_thm (get_current_shell ())
131     let edit_set_goal = edit_set_goal (get_current_shell ())
132     let edit_set_redex = edit_set_redex (get_current_shell ())
133     let edit_set_contractum = edit_set_contractum (get_current_shell ())
134     let edit_set_assumptions = edit_set_assumptions (get_current_shell ())
135     let edit_set_params = edit_set_params (get_current_shell ())
136     let edit_refine = edit_refine (get_current_shell ())
137     let edit_node = edit_node (get_current_shell ())
138     let edit_save = edit_save (get_current_shell ())
139     let edit_undo () = edit_undo (get_current_shell ())
140 jyh 2494
141 jyh 2775 let shell_get_term = Shell_state.ShellState.get_term
142    
143 jyh 2743 let _ = ShellHTTP.main ()
144 jyh 2494
145     (*
146     * -*-
147     * Local Variables:
148     * Caml-master: "refiner"
149     * End:
150     * -*-
151     *)

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26