X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fmatita%2FmatitaWiki.ml;h=87e9a44178a47a18b5bad6f9e9b3961e0825e71f;hb=48ccd3ca2b890b89775f1fbf7827bf617cf7aa19;hp=3beadf1fe185d4cae798b3bd3900c3f3564164fb;hpb=e465656be7e67ee3c02acf12a53c8388ae384b0a;p=helm.git diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml index 3beadf1fe..87e9a4417 100644 --- a/helm/software/matita/matitaWiki.ml +++ b/helm/software/matita/matitaWiki.ml @@ -34,13 +34,13 @@ exception AttemptToInsertAnAlias (** {2 Initialization} *) -let grafite_status = (ref None : GrafiteTypes.status option ref) -let lexicon_status = (ref None : LexiconEngine.status option ref) +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 - | Some ss, Some s -> ss,s + | ss::_, s::_ -> ss,s | _,_ -> assert false in let cb = fun _ _ -> () in @@ -49,8 +49,8 @@ let run_script is eval_function = match eval_function lexicon_status' grafite_status' is cb with [] -> raise End_of_file | ((grafite_status'',lexicon_status''),None)::_ -> - lexicon_status := Some lexicon_status''; - grafite_status := Some grafite_status'' + lexicon_status := lexicon_status''::!lexicon_status; + grafite_status := grafite_status''::!grafite_status | (s,Some _)::_ -> raise AttemptToInsertAnAlias with | GrafiteEngine.Drop @@ -63,81 +63,154 @@ let run_script is eval_function = raise exn let clean_exit n = - let opt_exit = - function - None -> () - | Some n -> exit n - in match !grafite_status with - None -> opt_exit n - | Some grafite_status -> - try - let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in + [] -> exit n + | grafite_status::_ -> + let baseuri = GrafiteTypes.get_baseuri grafite_status in LibraryClean.clean_baseuris ~verbose:false [baseuri]; - opt_exit n - with GrafiteTypes.Option_error("baseuri", "not found") -> - (* no baseuri ==> nothing to clean yet *) - opt_exit n + exit n -let terminate () = +let terminate n = let terminator = String.make 1 (Char.chr 249) in - print_endline terminator; - prerr_endline terminator + 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 () = terminate(); interactive_loop () in - let str = Ulexing.from_utf8_channel stdin in - let watch_statuses lexicon_status grafite_status = - match grafite_status.GrafiteTypes.proof_status with - GrafiteTypes.Incomplete_proof - {GrafiteTypes.proof = uri,metasenv,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 - (List.find (fun (j,_,_) -> j=i) metasenv) - ) open_goals)) - | _ -> () - in - let include_paths = - Helm_registry.get_list Helm_registry.string "matita.includes" in + let interactive_loop n = terminate n; interactive_loop () in try - run_script str - (MatitaEngine.eval_from_stream ~first_statement_only:true ~prompt:false - ~include_paths ~watch_statuses) ; - interactive_loop () + 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 () - | Sys.Break -> HLog.error "user break!"; interactive_loop () - | GrafiteTypes.Command_error _ -> interactive_loop () - | 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 () - | End_of_file as exn -> raise exn - | exn -> HLog.error (Printexc.to_string exn); interactive_loop () + | 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 -> "