X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2FmatitaWiki.ml;fp=matita%2FmatitaWiki.ml;h=87e9a44178a47a18b5bad6f9e9b3961e0825e71f;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/matita/matitaWiki.ml b/matita/matitaWiki.ml new file mode 100644 index 000000000..87e9a4417 --- /dev/null +++ b/matita/matitaWiki.ml @@ -0,0 +1,267 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(* $Id: matitacLib.ml 7090 2006-12-12 14:04:59Z fguidi $ *) + +open Printf + +open GrafiteTypes + +exception AttemptToInsertAnAlias + + +(** {2 Initialization} *) + +let grafite_status = (ref [] : GrafiteTypes.status list ref) +let lexicon_status = (ref [] : LexiconEngine.status list ref) + +let run_script is eval_function = + let lexicon_status',grafite_status' = + match !lexicon_status,!grafite_status with + | ss::_, s::_ -> ss,s + | _,_ -> assert false + in + let cb = fun _ _ -> () in + let matita_debug = Helm_registry.get_bool "matita.debug" in + try + match eval_function lexicon_status' grafite_status' is cb with + [] -> raise End_of_file + | ((grafite_status'',lexicon_status''),None)::_ -> + lexicon_status := lexicon_status''::!lexicon_status; + grafite_status := grafite_status''::!grafite_status + | (s,Some _)::_ -> raise AttemptToInsertAnAlias + with + | GrafiteEngine.Drop + | End_of_file + | CicNotationParser.Parse_error _ + | HExtlib.Localized _ as exn -> raise exn + | exn -> + if not matita_debug then + HLog.error (snd (MatitaExcPp.to_string exn)) ; + raise exn + +let clean_exit n = + match !grafite_status with + [] -> exit n + | grafite_status::_ -> + let baseuri = GrafiteTypes.get_baseuri grafite_status in + LibraryClean.clean_baseuris ~verbose:false [baseuri]; + exit n + +let terminate n = + let terminator = String.make 1 (Char.chr 249) in + let prompt = + (match n with + None -> "-1" + | Some n -> string_of_int n) ^ terminator + in + print_endline prompt; + prerr_endline prompt +;; + +let outer_syntax_parser () = + let text = ref "" in + let tag = ref `Do in + let callbacks = + { XmlPushParser.default_callbacks with + XmlPushParser.start_element = + (Some + (fun name attrs -> + match name with + "pgip" -> () + | "doitem" -> tag := `Do + | "undoitem" -> tag := `Undo + | _ -> assert false)) ; + XmlPushParser.character_data = + (Some (fun s -> text := !text ^ s)) ; + XmlPushParser.end_element = + (Some + (function + "pgip" -> raise (XmlPushParser.Parse_error "EOC") + | "doitem" + | "undoitem" -> () + | _ -> assert false)) + } + in + let parse = XmlPushParser.create_parser callbacks in + try + XmlPushParser.parse parse (`Channel stdin) ; + raise End_of_file + with + XmlPushParser.Parse_error "no element found" -> raise End_of_file + | XmlPushParser.Parse_error "EOC" -> + match !tag with + `Do -> `Do !text + | `Undo -> + try + `Undo (int_of_string !text) + with + Failure _ -> assert false +;; + +let include_paths = + lazy (Helm_registry.get_list Helm_registry.string "matita.includes") +;; + +let rec interactive_loop () = + (* every loop is terminated by a terminator both on stdout and stderr *) + let interactive_loop n = terminate n; interactive_loop () in + try + match outer_syntax_parser () with + `Undo n -> + let rec drop = + function + 0,l -> l + | n,_::l -> drop (n-1,l) + | _,[] -> assert false + in + let to_be_dropped = List.length !lexicon_status - n in + let safe_hd = function [] -> assert false | he::_ -> he in + let cur_lexicon_status = safe_hd !lexicon_status in + let cur_grafite_status = safe_hd !grafite_status in + lexicon_status := drop (to_be_dropped, !lexicon_status) ; + grafite_status := drop (to_be_dropped, !grafite_status) ; + let lexicon_status = safe_hd !lexicon_status in + let grafite_status = safe_hd !grafite_status in + LexiconSync.time_travel + ~present:cur_lexicon_status ~past:lexicon_status; + GrafiteSync.time_travel + ~present:cur_grafite_status ~past:grafite_status; + interactive_loop (Some n) + | `Do command -> + let str = Ulexing.from_utf8_string command in + let watch_statuses lexicon_status grafite_status = + match grafite_status.GrafiteTypes.proof_status with + GrafiteTypes.Incomplete_proof + {GrafiteTypes.proof = uri,metasenv,_subst,bo,ty,attrs ; + GrafiteTypes.stack = stack } -> + let open_goals = Continuationals.Stack.open_goals stack in + print_endline + (String.concat "\n" + (List.map + (fun i -> + ApplyTransformation.txt_of_cic_sequent 80 metasenv + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") + (List.find (fun (j,_,_) -> j=i) metasenv) + ) open_goals)) + | _ -> () + in + run_script str + (MatitaEngine.eval_from_stream ~first_statement_only:true + ~include_paths:(Lazy.force include_paths) ~watch_statuses) ; + interactive_loop (Some (List.length !lexicon_status)) + with + | GrafiteEngine.Macro (floc,_) -> + let x, y = HExtlib.loc_of_floc floc in + HLog.error + (sprintf "A macro has been found in a script at %d-%d" x y); + interactive_loop None + | Sys.Break -> HLog.error "user break!"; interactive_loop None + | GrafiteTypes.Command_error _ -> interactive_loop None + | HExtlib.Localized (floc,CicNotationParser.Parse_error err) -> + let x, y = HExtlib.loc_of_floc floc in + HLog.error (sprintf "Parse error at %d-%d: %s" x y err); + interactive_loop None + | End_of_file as exn -> raise exn + | exn -> HLog.error (Printexc.to_string exn); interactive_loop None + + +let main () = + MatitaInit.initialize_all (); + HLog.set_log_callback + (fun tag msg -> + let s = + match tag with + `Debug -> "