1 (* Copyright (C) 2004-2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
26 (* $Id: matitacLib.ml 7090 2006-12-12 14:04:59Z fguidi $ *)
32 exception AttemptToInsertAnAlias
35 (** {2 Initialization} *)
37 let grafite_status = (ref [] : GrafiteTypes.status list ref)
39 let run_script is eval_function =
41 match !grafite_status with
45 let cb = fun _ _ -> () in
46 let matita_debug = Helm_registry.get_bool "matita.debug" in
48 match eval_function grafite_status' is cb with
49 [] -> raise End_of_file
50 | (grafite_status'',None)::_ ->
51 grafite_status := grafite_status''::!grafite_status
52 | (s,Some _)::_ -> raise AttemptToInsertAnAlias
56 | CicNotationParser.Parse_error _
57 | HExtlib.Localized _ as exn -> raise exn
59 if not matita_debug then
60 HLog.error (snd (MatitaExcPp.to_string exn)) ;
64 match !grafite_status with
66 | grafite_status::_ ->
67 let baseuri = GrafiteTypes.get_baseuri grafite_status in
68 LibraryClean.clean_baseuris ~verbose:false [baseuri];
72 let terminator = String.make 1 (Char.chr 249) in
76 | Some n -> string_of_int n) ^ terminator
82 let outer_syntax_parser () =
86 { XmlPushParser.default_callbacks with
87 XmlPushParser.start_element =
92 | "doitem" -> tag := `Do
93 | "undoitem" -> tag := `Undo
94 | _ -> assert false)) ;
95 XmlPushParser.character_data =
96 (Some (fun s -> text := !text ^ s)) ;
97 XmlPushParser.end_element =
100 "pgip" -> raise (XmlPushParser.Parse_error "EOC")
103 | _ -> assert false))
106 let parse = XmlPushParser.create_parser callbacks in
108 XmlPushParser.parse parse (`Channel stdin) ;
111 XmlPushParser.Parse_error "no element found" -> raise End_of_file
112 | XmlPushParser.Parse_error "EOC" ->
117 `Undo (int_of_string !text)
119 Failure _ -> assert false
123 lazy (Helm_registry.get_list Helm_registry.string "matita.includes")
126 let rec interactive_loop () =
127 (* every loop is terminated by a terminator both on stdout and stderr *)
128 let interactive_loop n = terminate n; interactive_loop () in
130 match outer_syntax_parser () with
135 | n,_::l -> drop (n-1,l)
136 | _,[] -> assert false
138 let to_be_dropped = List.length !grafite_status - n in
139 let safe_hd = function [] -> assert false | he::_ -> he in
140 let cur_grafite_status = safe_hd !grafite_status in
141 grafite_status := drop (to_be_dropped, !grafite_status) ;
142 let grafite_status = safe_hd !grafite_status in
143 LexiconSync.time_travel
144 ~present:(GrafiteTypes.get_estatus cur_grafite_status)
145 ~past:(GrafiteTypes.get_estatus grafite_status);
146 GrafiteSync.time_travel
147 ~present:cur_grafite_status ~past:grafite_status;
148 interactive_loop (Some n)
150 let str = Ulexing.from_utf8_string command in
151 let watch_statuses grafite_status =
152 match grafite_status.GrafiteTypes.proof_status with
153 GrafiteTypes.Incomplete_proof
154 {GrafiteTypes.proof = uri,metasenv,_subst,bo,ty,attrs ;
155 GrafiteTypes.stack = stack } ->
156 let open_goals = Continuationals.Stack.open_goals stack in
161 ApplyTransformation.txt_of_cic_sequent 80 metasenv
162 ~map_unicode_to_tex:(Helm_registry.get_bool
163 "matita.paste_unicode_as_tex")
164 (List.find (fun (j,_,_) -> j=i) metasenv)
169 (MatitaEngine.eval_from_stream ~first_statement_only:true
170 ~include_paths:(Lazy.force include_paths) ~watch_statuses) ;
171 interactive_loop (Some (List.length !grafite_status))
173 | GrafiteEngine.Macro (floc,_) ->
174 let x, y = HExtlib.loc_of_floc floc in
176 (sprintf "A macro has been found in a script at %d-%d" x y);
177 interactive_loop None
178 | Sys.Break -> HLog.error "user break!"; interactive_loop None
179 | GrafiteTypes.Command_error _ -> interactive_loop None
180 | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
181 let x, y = HExtlib.loc_of_floc floc in
182 HLog.error (sprintf "Parse error at %d-%d: %s" x y err);
183 interactive_loop None
184 | End_of_file as exn -> raise exn
185 | exn -> HLog.error (Printexc.to_string exn); interactive_loop None
189 MatitaInit.initialize_all ();
190 HLog.set_log_callback
194 `Debug -> "<div style='color:blue'>Debug: " ^ msg ^ "</div><br/>\n"
195 | `Message -> "<div style='color:green'>Info: " ^ msg ^ "</div><br/>\n"
196 | `Warning -> "<div style='color:yellow'>Warn: " ^ msg ^ "</div><br/>\n"
197 | `Error -> "<div style='color:red'>Error: " ^ msg ^ "</div><br/>\n"
199 output_string stderr s;
202 (* must be called after init since args are set by cmdline parsing *)
203 let system_mode = Helm_registry.get_bool "matita.system" in
205 Helm_registry.get_list Helm_registry.string "matita.includes" in
206 grafite_status := [GrafiteSync.init (CicNotation2.load_notation ~include_paths
207 (new LexiconEngine.status) BuildTimeConf.core_notation_script) "cic:/matita/tests/"];
208 Sys.catch_break true;
209 let origcb = HLog.get_log_callback () in
210 let origcb t s = origcb t ((if system_mode then "[S] " else "") ^ s) in
214 | `Message | `Warning | `Error -> origcb tag s
216 HLog.set_log_callback newcb;
217 let matita_debug = Helm_registry.get_bool "matita.debug" in
223 | GrafiteEngine.Drop -> clean_exit 1
225 let proof_status,moo_content_rev,lexicon_content_rev,dump =
226 match !grafite_status with
228 s.proof_status, s.moo_content_rev,
229 (GrafiteTypes.get_estatus s)#lstatus.LexiconEngine.lexicon_content_rev,
230 (GrafiteTypes.get_estatus s)#dump
233 if proof_status <> GrafiteTypes.No_proof then
236 "there are still incomplete proofs at the end of the script";
242 GrafiteTypes.get_baseuri
243 (match !grafite_status with
248 LibraryMisc.obj_file_of_baseuri
249 ~must_exist:false ~baseuri ~writable:true
252 LibraryMisc.lexicon_file_of_baseuri
253 ~must_exist:false ~baseuri ~writable:true
255 GrafiteMarshal.save_moo moo_fname moo_content_rev;
256 LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
257 NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) dump;
262 if matita_debug then raise exn;