]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/matitaWiki.ml
matita-icon
[helm.git] / helm / software / matita / matitaWiki.ml
1 (* Copyright (C) 2004-2005, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 (* $Id: matitacLib.ml 7090 2006-12-12 14:04:59Z fguidi $ *)
27
28 open Printf
29
30 open GrafiteTypes
31
32 exception AttemptToInsertAnAlias
33
34
35 (** {2 Initialization} *)
36
37 let grafite_status = (ref [] : GrafiteTypes.status list ref)
38 let lexicon_status = (ref [] : LexiconEngine.status list ref)
39
40 let run_script is eval_function  =
41   let lexicon_status',grafite_status' = 
42     match !lexicon_status,!grafite_status with
43     | ss::_, s::_ -> ss,s
44     | _,_ -> assert false
45   in
46   let cb = fun _ _ -> () in
47   let matita_debug = Helm_registry.get_bool "matita.debug" in
48   try
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 := lexicon_status''::!lexicon_status;
53        grafite_status := grafite_status''::!grafite_status
54     | (s,Some _)::_ -> raise AttemptToInsertAnAlias
55   with
56   | GrafiteEngine.Drop  
57   | End_of_file
58   | CicNotationParser.Parse_error _
59   | HExtlib.Localized _ as exn -> raise exn
60   | exn -> 
61       if not matita_debug then
62        HLog.error (snd (MatitaExcPp.to_string exn)) ;
63       raise exn
64
65 let clean_exit n =
66   match !grafite_status with
67      [] -> exit n
68    | grafite_status::_ ->
69       try
70        let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in
71        LibraryClean.clean_baseuris ~verbose:false [baseuri];
72        exit n
73       with GrafiteTypes.Option_error("baseuri", "not found") ->
74        (* no baseuri ==> nothing to clean yet *)
75        exit n
76
77 let terminate n =
78  let terminator = String.make 1 (Char.chr 249) in
79  let prompt =
80   (match n with
81      None -> "-1"
82    | Some n -> string_of_int n) ^ terminator
83  in
84   print_endline prompt;
85   prerr_endline prompt
86 ;;
87
88 let outer_syntax_parser () =
89  let text = ref "" in
90  let tag = ref `Do in
91  let callbacks =
92   { XmlPushParser.default_callbacks with
93     XmlPushParser.start_element =
94      (Some
95        (fun name attrs ->
96          match name with
97             "pgip" -> ()
98           | "doitem" -> tag := `Do
99           | "undoitem" -> tag := `Undo
100           | _ -> assert false)) ;
101     XmlPushParser.character_data =
102      (Some (fun s -> text := !text ^ s)) ;
103     XmlPushParser.end_element =
104      (Some
105        (function
106            "pgip" -> raise (XmlPushParser.Parse_error "EOC")
107          | "doitem"
108          | "undoitem" -> ()
109          | _ -> assert false))
110   }
111  in
112   let parse = XmlPushParser.create_parser callbacks in
113     try
114      XmlPushParser.parse parse (`Channel stdin) ;
115      raise End_of_file
116     with
117        XmlPushParser.Parse_error "no element found" -> raise End_of_file
118      | XmlPushParser.Parse_error "EOC" ->
119         match !tag with
120            `Do -> `Do !text
121          | `Undo ->
122              try
123               `Undo (int_of_string !text)
124              with
125               Failure _ -> assert false
126 ;;
127
128 let include_paths =
129  lazy (Helm_registry.get_list Helm_registry.string "matita.includes")
130 ;;
131   
132 let rec interactive_loop () = 
133   (* every loop is terminated by a terminator both on stdout and stderr *)
134   let interactive_loop n = terminate n; interactive_loop () in
135   try
136    match outer_syntax_parser () with
137       `Undo n ->
138         let rec drop =
139          function
140             0,l -> l
141           | n,_::l -> drop (n-1,l)
142           | _,[] -> assert false
143         in
144          let to_be_dropped = List.length !lexicon_status - n in
145          let safe_hd = function [] -> assert false | he::_ -> he in
146          let cur_lexicon_status = safe_hd !lexicon_status in
147          let cur_grafite_status = safe_hd !grafite_status in
148           lexicon_status := drop (to_be_dropped, !lexicon_status) ;
149           grafite_status := drop (to_be_dropped, !grafite_status) ;
150           let lexicon_status = safe_hd !lexicon_status in
151           let grafite_status = safe_hd !grafite_status in
152            LexiconSync.time_travel
153             ~present:cur_lexicon_status ~past:lexicon_status;
154            GrafiteSync.time_travel
155             ~present:cur_grafite_status ~past:grafite_status;
156            interactive_loop (Some n)
157     | `Do command ->
158         let str = Ulexing.from_utf8_string command in
159         let watch_statuses lexicon_status grafite_status =
160          match grafite_status.GrafiteTypes.proof_status with
161             GrafiteTypes.Incomplete_proof
162              {GrafiteTypes.proof = uri,metasenv,_subst,bo,ty,attrs ;
163               GrafiteTypes.stack = stack } ->
164               let open_goals = Continuationals.Stack.open_goals stack in
165               print_endline
166                (String.concat "\n"
167                  (List.map
168                    (fun i ->
169                      ApplyTransformation.txt_of_cic_sequent 80 metasenv
170                       ~map_unicode_to_tex:(Helm_registry.get_bool
171                         "matita.paste_unicode_as_tex")
172                       (List.find (fun (j,_,_) -> j=i) metasenv)
173                    ) open_goals))
174           | _ -> ()
175         in
176          run_script str 
177            (MatitaEngine.eval_from_stream ~first_statement_only:true ~prompt:false
178            ~include_paths:(Lazy.force include_paths) ~watch_statuses) ;
179          interactive_loop (Some (List.length !lexicon_status))
180   with 
181    | GrafiteEngine.Macro (floc,_) ->
182       let x, y = HExtlib.loc_of_floc floc in
183        HLog.error
184         (sprintf "A macro has been found in a script at %d-%d" x y);
185        interactive_loop None
186    | Sys.Break -> HLog.error "user break!"; interactive_loop None
187    | GrafiteTypes.Command_error _ -> interactive_loop None
188    | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
189       let x, y = HExtlib.loc_of_floc floc in
190        HLog.error (sprintf "Parse error at %d-%d: %s" x y err);
191        interactive_loop None
192    | End_of_file as exn -> raise exn
193    | exn -> HLog.error (Printexc.to_string exn); interactive_loop None
194
195
196 let main () = 
197   MatitaInit.initialize_all ();
198   HLog.set_log_callback
199    (fun tag msg ->
200      let s =
201       match tag with
202          `Debug -> "<div style='color:blue'>Debug: " ^ msg ^ "</div><br/>\n"
203        | `Message -> "<div style='color:green'>Info: " ^ msg ^ "</div><br/>\n"
204        | `Warning -> "<div style='color:yellow'>Warn: " ^ msg ^ "</div><br/>\n"
205        | `Error -> "<div style='color:red'>Error: " ^ msg ^ "</div><br/>\n"
206      in
207       output_string stderr s;
208       flush stderr
209    );
210   (* must be called after init since args are set by cmdline parsing *)
211   let system_mode =  Helm_registry.get_bool "matita.system" in
212   Helm_registry.set_int "matita.verbosity" 0;
213   let include_paths =
214    Helm_registry.get_list Helm_registry.string "matita.includes" in
215   grafite_status := [GrafiteSync.init ()];
216   lexicon_status :=
217    [CicNotation2.load_notation ~include_paths
218      BuildTimeConf.core_notation_script] ;
219   Sys.catch_break true;
220   let origcb = HLog.get_log_callback () in
221   let origcb t s = origcb t ((if system_mode then "[S] " else "") ^ s) in
222   let newcb tag s =
223     match tag with
224     | `Debug -> ()
225     | `Message | `Warning | `Error -> origcb tag s
226   in
227   HLog.set_log_callback newcb;
228   let matita_debug = Helm_registry.get_bool "matita.debug" in
229   try
230     (try
231       interactive_loop ()
232      with
233       | End_of_file -> ()
234       | GrafiteEngine.Drop -> clean_exit 1
235     );
236     let proof_status,moo_content_rev,lexicon_content_rev = 
237       match !lexicon_status,!grafite_status with
238       | ss::_, s::_ ->
239          s.proof_status, s.moo_content_rev,
240           ss.LexiconEngine.lexicon_content_rev
241       | _,_ -> assert false
242     in
243     if proof_status <> GrafiteTypes.No_proof then
244      begin
245       HLog.error
246        "there are still incomplete proofs at the end of the script";
247       clean_exit 2
248      end
249     else
250      begin
251        let baseuri =
252         GrafiteTypes.get_string_option
253          (match !grafite_status with
254              [] -> assert false
255            | s::_ -> s) "baseuri" in
256        let moo_fname = 
257          LibraryMisc.obj_file_of_baseuri 
258            ~must_exist:false ~baseuri ~writable:true 
259        in
260        let lexicon_fname= 
261          LibraryMisc.lexicon_file_of_baseuri 
262           ~must_exist:false ~baseuri ~writable:true 
263        in
264        GrafiteMarshal.save_moo moo_fname moo_content_rev;
265        LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
266        exit 0
267      end
268   with 
269   | exn ->
270       if matita_debug then raise exn;
271       clean_exit 3