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 None : GrafiteTypes.status option ref)
38 let lexicon_status = (ref None : LexiconEngine.status option ref)
40 let run_script is eval_function =
41 let lexicon_status',grafite_status' =
42 match !lexicon_status,!grafite_status with
43 | Some ss, Some s -> ss,s
46 let cb = fun _ _ -> () in
47 let matita_debug = Helm_registry.get_bool "matita.debug" in
49 match eval_function lexicon_status' grafite_status' is cb with
50 [] -> raise End_of_file
51 | ((grafite_status'',lexicon_status''),None)::_ ->
52 lexicon_status := Some lexicon_status'';
53 grafite_status := Some grafite_status''
54 | (s,Some _)::_ -> raise AttemptToInsertAnAlias
58 | CicNotationParser.Parse_error _
59 | HExtlib.Localized _ as exn -> raise exn
61 if not matita_debug then
62 HLog.error (snd (MatitaExcPp.to_string exn)) ;
71 match !grafite_status with
73 | Some grafite_status ->
75 let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in
76 LibraryClean.clean_baseuris ~verbose:false [baseuri];
78 with GrafiteTypes.Option_error("baseuri", "not found") ->
79 (* no baseuri ==> nothing to clean yet *)
83 let terminator = String.make 1 (Char.chr 249) in
84 print_endline terminator;
85 prerr_endline terminator
88 let rec interactive_loop () =
89 (* every loop is terminated by a terminator both on stdout and stderr *)
90 let interactive_loop () = terminate(); interactive_loop () in
91 let str = Ulexing.from_utf8_channel stdin in
92 let watch_statuses lexicon_status grafite_status =
93 match grafite_status.GrafiteTypes.proof_status with
94 GrafiteTypes.Incomplete_proof
95 {GrafiteTypes.proof = uri,metasenv,bo,ty,attrs ;
96 GrafiteTypes.stack = stack } ->
97 let open_goals = Continuationals.Stack.open_goals stack in
102 ApplyTransformation.txt_of_cic_sequent 80 metasenv
103 (List.find (fun (j,_,_) -> j=i) metasenv)
108 Helm_registry.get_list Helm_registry.string "matita.includes" in
111 (MatitaEngine.eval_from_stream ~first_statement_only:true ~prompt:false
112 ~include_paths ~watch_statuses) ;
115 | GrafiteEngine.Macro (floc,_) ->
116 let x, y = HExtlib.loc_of_floc floc in
118 (sprintf "A macro has been found in a script at %d-%d" x y);
120 | Sys.Break -> HLog.error "user break!"; interactive_loop ()
121 | GrafiteTypes.Command_error _ -> interactive_loop ()
122 | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
123 let x, y = HExtlib.loc_of_floc floc in
124 HLog.error (sprintf "Parse error at %d-%d: %s" x y err);
126 | End_of_file as exn -> raise exn
127 | exn -> HLog.error (Printexc.to_string exn); interactive_loop ()
131 MatitaInit.initialize_all ();
132 (* must be called after init since args are set by cmdline parsing *)
133 let system_mode = Helm_registry.get_bool "matita.system" in
134 Helm_registry.set_int "matita.verbosity" 0;
136 Helm_registry.get_list Helm_registry.string "matita.includes" in
137 grafite_status := Some (GrafiteSync.init ());
139 Some (CicNotation2.load_notation ~include_paths
140 BuildTimeConf.core_notation_script);
141 Sys.catch_break true;
142 let origcb = HLog.get_log_callback () in
143 let origcb t s = origcb t ((if system_mode then "[S] " else "") ^ s) in
147 | `Message | `Warning | `Error -> origcb tag s
149 HLog.set_log_callback newcb;
150 let matita_debug = Helm_registry.get_bool "matita.debug" in
156 | GrafiteEngine.Drop -> clean_exit (Some 1)
158 let proof_status,moo_content_rev,metadata,lexicon_content_rev =
159 match !lexicon_status,!grafite_status with
161 s.proof_status, s.moo_content_rev, ss.LexiconEngine.metadata,
162 ss.LexiconEngine.lexicon_content_rev
163 | _,_ -> assert false
165 if proof_status <> GrafiteTypes.No_proof then
168 "there are still incomplete proofs at the end of the script";
174 GrafiteTypes.get_string_option
175 (match !grafite_status with
177 | Some s -> s) "baseuri" in
179 LibraryMisc.obj_file_of_baseuri
180 ~must_exist:false ~baseuri ~writable:true
183 LibraryMisc.lexicon_file_of_baseuri
184 ~must_exist:false ~baseuri ~writable:true
187 LibraryMisc.metadata_file_of_baseuri
188 ~must_exist:false ~baseuri ~writable:true
190 GrafiteMarshal.save_moo moo_fname moo_content_rev;
191 LibraryNoDb.save_metadata metadata_fname metadata;
192 LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
197 if matita_debug then raise exn;