X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=4738a38f673dd55bd6b6496358b655194007a32f;hb=647b419e96770d90a82d7a9e5e8843566a9f93ee;hp=9e0f85b5842536f1da2466b2430850cf2adb2e06;hpb=6719c0e318b312b51b089fea3d69d1b7103245ea;p=helm.git diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 9e0f85b58..4738a38f6 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -71,12 +71,9 @@ type guistuff = { ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL]; } -let eval_with_engine include_paths guistuff lexicon_status grafite_status user_goal +let eval_with_engine include_paths guistuff grafite_status user_goal skipped_txt nonskipped_txt st = - let module TAPp = GrafiteAstPp in - let module DTE = DisambiguateTypes.Environment in - let module DP = DisambiguatePp in let parsed_text_length = String.length skipped_txt + String.length nonskipped_txt in @@ -85,7 +82,7 @@ let eval_with_engine include_paths guistuff lexicon_status grafite_status user_g let enriched_history_fragment = MatitaEngine.eval_ast ~do_heavy_checks:(Helm_registry.get_bool "matita.do_heavy_checks") - lexicon_status grafite_status (text,prefix_len,st) + grafite_status (text,prefix_len,st) in let enriched_history_fragment = List.rev enriched_history_fragment in (* really fragile *) @@ -94,8 +91,8 @@ let eval_with_engine include_paths guistuff lexicon_status grafite_status user_g (fun (acc, to_prepend) (status,alias) -> match alias with | None -> (status,to_prepend ^ nonskipped_txt)::acc,"" - | Some (k,((v,_) as value)) -> - let newtxt = DP.pp_environment (DTE.add k value DTE.empty) in + | Some (k,value) -> + let newtxt = LexiconAstPp.pp_alias value in (status,to_prepend ^ newtxt ^ "\n")::acc, "") ([],skipped_txt) enriched_history_fragment in @@ -106,7 +103,7 @@ let eval_with_engine include_paths guistuff lexicon_status grafite_status user_g * so that we can ensure the inclusion is performed after the included file * is compiled (if needed). matitac does not need that, since it compiles files * in the good order, here files may be compiled on demand. *) -let wrap_with_make include_paths (f : GrafiteParser.statement) x = +let wrap_with_make include_paths (f : #LexiconEngine.status GrafiteParser.statement) x = try f ~never_include:true ~include_paths x with @@ -118,28 +115,7 @@ let wrap_with_make include_paths (f : GrafiteParser.statement) x = HLog.error "please create it."; raise (Failure ("No root file for "^mafilename)) in - let initial_lexicon_status = - CicNotation2.load_notation ~include_paths:[] BuildTimeConf.core_notation_script - in - let b,x = - try - GrafiteSync.push (); - LexiconSync.time_travel ~present:x ~past:initial_lexicon_status; - let rc = MatitacLib.Make.make root [tgt] in - GrafiteSync.pop (); - CicNotation.reset (); - ignore(CicNotation2.load_notation ~include_paths:[] - BuildTimeConf.core_notation_script); - let x = List.fold_left (fun s c -> LexiconEngine.eval_command s c) - initial_lexicon_status (List.rev - x.LexiconEngine.lexicon_content_rev) - in - rc,x - with - | exn -> - HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn)); - assert false - in + let b = MatitacLib.Make.make root [tgt] in if b then try f ~include_paths x with LexiconEngine.IncludedFileNotCompiled _ -> raise @@ -234,7 +210,7 @@ let cic2grafite context menv t = | Cic.Const _ as t -> PT.Ident (pp_t c t, None) | Cic.Appl l -> PT.Appl (List.map (aux c) l) - | Cic.Implicit _ -> PT.Implicit + | Cic.Implicit _ -> PT.Implicit `JustOne | Cic.Lambda (Cic.Name n, s, t) -> PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)), aux (Some (Cic.Name n, Cic.Decl s)::c) t) @@ -244,7 +220,7 @@ let cic2grafite context menv t = | Cic.LetIn (Cic.Name n, s, ty, t) -> PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)), aux (Some (Cic.Name n, Cic.Def (s,ty))::c) t) - | Cic.Meta _ -> PT.Implicit + | Cic.Meta _ -> PT.Implicit `JustOne | Cic.Sort (Cic.Type u) -> PT.Sort (`Type u) | Cic.Sort Cic.Set -> PT.Sort `Set | Cic.Sort (Cic.CProp u) -> PT.Sort (`CProp u) @@ -368,8 +344,8 @@ let cic2grafite context menv t = let width = max_int in let term_pp content_term = let pres_term = TermContentPres.pp_ast content_term in - let dummy_tbl = Hashtbl.create 1 in - let markup = CicNotationPres.render dummy_tbl pres_term in + let lookup_uri = fun _ -> None in + let markup = CicNotationPres.render ~lookup_uri pres_term in let s = "(" ^ BoxPp.render_to_string ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") @@ -389,43 +365,90 @@ let cic2grafite context menv t = prerr_endline script; stupid_indenter script ;; +let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac = + let parsed_text_length = String.length parsed_text in + match mac with + | TA.Screenshot (_,name) -> + let status = script#grafite_status in + let _,_,menv,subst,_ = status#obj in + let name = Filename.dirname (script#filename) ^ "/" ^ name in + let sequents = + let selected = Continuationals.Stack.head_goals status#stack in + List.filter (fun x,_ -> List.mem x selected) menv + in + guistuff.mathviewer#screenshot status sequents menv subst name; + [status, parsed_text], "", parsed_text_length + | TA.NCheck (_,t) -> + let status = script#grafite_status in + let _,_,menv,subst,_ = status#obj in + let ctx = + try let _,(_,ctx,_) = List.hd menv in ctx + with Failure "hd" -> [] + in + let m, s, status, t = + GrafiteDisambiguate.disambiguate_nterm + None status ctx menv subst (parsed_text,parsed_text_length, + CicNotationPt.Cast (t,CicNotationPt.Implicit `JustOne)) + (* XXX use the metasenv, if possible *) + in + guistuff.mathviewer#show_entry (`NCic (t,ctx,m,s)); + [status, parsed_text], "", parsed_text_length + | TA.NIntroGuess _loc -> + let names_ref = ref [] in + let s = + NTactics.intros_tac ~names_ref [] script#grafite_status + in + let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in + let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in + [s, nl ^ "#" ^ String.concat " " !names_ref ^ ";"], "", parsed_text_length + | TA.NAutoInteractive (_loc, (None,a)) -> + let trace_ref = ref [] in + let s = + NnAuto.auto_tac + ~params:(None,a) ~trace_ref script#grafite_status + in + let depth = + try List.assoc "depth" a + with Not_found -> "" + in + let trace = "/"^(if int_of_string depth > 1 then depth else "")^"/ by " in + let thms = + match !trace_ref with + | [] -> "{}" + | thms -> + String.concat ", " + (HExtlib.filter_map (function + | CicNotationPt.NRef r -> Some (NCicPp.r2s true r) + | _ -> None) + thms) + in + let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in + let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in + [s, nl ^ trace ^ thms ^ ";"], "", parsed_text_length + | TA.NAutoInteractive (_, (Some _,_)) -> assert false -let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script mac = - let module TAPp = GrafiteAstPp in +let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac = let module MQ = MetadataQuery in - let module MDB = LibraryDb in let module CTC = CicTypeChecker in - let module CU = CicUniv in (* no idea why ocaml wants this *) let parsed_text_length = String.length parsed_text in let dbd = LibraryDb.instance () in - let pp_macro = - let f t = ProofEngineReduction.replace - ~equality:(fun _ t -> match t with Cic.Meta _ -> true | _ -> false) - ~what:[()] ~with_what:[Cic.Implicit None] ~where:t - in - let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in - TAPp.pp_macro - ~term_pp:(fun x -> - ApplyTransformation.txt_of_cic_term max_int metasenv [] (f x) - ~map_unicode_to_tex:(Helm_registry.get_bool - "matita.paste_unicode_as_tex")) - in + let pp_macro = ApplyTransformation.txt_of_macro ~map_unicode_to_tex:false in match mac with (* WHELP's stuff *) | TA.WMatch (loc, term) -> let l = Whelp.match_term ~dbd term in - let entry = `Whelp (pp_macro mac, l) in + let entry = `Whelp (pp_macro [] [] mac, l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], "", parsed_text_length | TA.WInstance (loc, term) -> let l = Whelp.instance ~dbd term in - let entry = `Whelp (pp_macro mac, l) in + let entry = `Whelp (pp_macro [] [] mac, l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], "", parsed_text_length | TA.WLocate (loc, s) -> let l = Whelp.locate ~dbd s in - let entry = `Whelp (pp_macro mac, l) in + let entry = `Whelp (pp_macro [] [] mac, l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], "", parsed_text_length | TA.WElim (loc, term) -> @@ -435,14 +458,14 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status | _ -> failwith "Not a MutInd" in let l = Whelp.elim ~dbd uri in - let entry = `Whelp (pp_macro mac, l) in + let entry = `Whelp (pp_macro [] [] mac, l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], "", parsed_text_length | TA.WHint (loc, term) -> let _subst = [] in - let s = ((None,[0,[],term], _subst, Cic.Meta (0,[]) ,term, []),0) in + let s = ((None,[0,[],term], _subst, lazy (Cic.Meta (0,[])) ,term, []),0) in let l = List.map fst (MQ.experimental_hint ~dbd s) in - let entry = `Whelp (pp_macro mac, l) in + let entry = `Whelp (pp_macro [] [] mac, l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], "", parsed_text_length (* REAL macro *) @@ -457,7 +480,8 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status if rewrite then let l = MQ.equations_for_goal ~dbd proof_status in let l = List.filter (fun u -> not (LibraryObjects.in_eq_URIs u)) l in - let entry = `Whelp (pp_macro (TA.WHint(loc, Cic.Implicit None)), l) in + let entry = + `Whelp (pp_macro [] [] (TA.WHint(loc, Cic.Implicit None)), l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], "", parsed_text_length else @@ -481,7 +505,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status let loc = HExtlib.floc_of_loc (0,text_len) in let statement = `Ast (GrafiteParser.LSome (ast loc),text) in let res,_,_parsed_text_len = - eval_statement include_paths buffer guistuff lexicon_status + eval_statement include_paths buffer guistuff grafite_status user_goal script statement in (* we need to replace all the parsed_text *) @@ -493,6 +517,32 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status fun u -> HLog.error (UriManager.string_of_uri u ^ "\n") ) selected; assert false) + | TA.Eval (_, kind, term) -> + let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in + let context = + match user_goal with + None -> [] + | Some n -> GrafiteTypes.get_proof_context grafite_status n in + let ty,_ = CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph in + let term = + match kind with + | `Normalize -> + CicReduction.normalize ~delta:true ~subst:[] context term + | `Simpl -> + ProofEngineReduction.simpl context term + | `Unfold None -> + ProofEngineReduction.unfold ?what:None context term + | `Unfold (Some lazy_term) -> + let what, _, _ = + lazy_term context metasenv CicUniv.empty_ugraph in + ProofEngineReduction.unfold ~what context term + | `Whd -> + CicReduction.whd ~delta:true ~subst:[] context term + in + let t_and_ty = Cic.Cast (term,ty) in + guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv)); + [(grafite_status#set_proof_status No_proof), parsed_text ],"", + parsed_text_length | TA.Check (_,term) -> let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in let context = @@ -518,7 +568,8 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status let (_,menv,subst,_,_,_), _ = ProofEngineTypes.apply_tactic (Auto.auto_tac ~dbd ~params - ~universe:grafite_status.GrafiteTypes.universe) proof_status + ~automation_cache:grafite_status#automation_cache) + proof_status in let proof_term = let irl = @@ -541,45 +592,31 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status in let ty,_ = CicTypeChecker.type_of_aux' - menv [] proof_term CicUniv.empty_ugraph + [] [] proof_term CicUniv.empty_ugraph in - prerr_endline (CicPp.ppterm proof_term); + prerr_endline (CicPp.ppterm proof_term ^ " n lambda= " ^ string_of_int how_many_lambdas); (* use declarative output *) let obj = (* il proof_term vive in cc, devo metterci i lambda no? *) - (Cic.CurrentProof ("xxx",menv,proof_term,ty,[],[])) + (Cic.CurrentProof ("xxx",[],proof_term,ty,[],[])) in ApplyTransformation.txt_of_cic_object ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") ~skip_thm_and_qed:true ~skip_initial_lambdas:how_many_lambdas - 80 GrafiteAst.Declarative "" obj + 80 [] obj else if true then (* use cic2grafite *) cic2grafite cc menv proof_term else (* alternative using FG stuff *) - let proof_term, how_many_lambdas = - Auto.lambda_close ~prefix_name:"orrible_hack_" - proof_term menv cc - in - let ty,_ = - CicTypeChecker.type_of_aux' - menv [] proof_term CicUniv.empty_ugraph - in - let obj = - Cic.Constant ("",Some proof_term, ty, [], [`Flavour `Lemma]) - in - Pcre.qreplace ~templ:"?" ~pat:"orrible_hack_[0-9]+" - (strip_comments - (ApplyTransformation.txt_of_cic_object - ~map_unicode_to_tex:(Helm_registry.get_bool - "matita.paste_unicode_as_tex") - ~skip_thm_and_qed:true - ~skip_initial_lambdas:how_many_lambdas - 80 (GrafiteAst.Procedural None) "" obj)) + let map_unicode_to_tex = + Helm_registry.get_bool "matita.paste_unicode_as_tex" + in + ApplyTransformation.procedural_txt_of_cic_term + ~map_unicode_to_tex 78 [] cc proof_term in let text = comment parsed_text ^ "\n" ^ proof_script ^ trailer in [],text,parsed_text_length @@ -587,28 +624,25 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status ProofEngineTypes.Fail _ as exn -> raise exn (* [], comment parsed_text ^ "\nfail.\n", parsed_text_length *)) - | TA.Inline (_,style,suri,prefix) -> - let str = + | TA.Inline (_, suri, params) -> + let str = "\n\n" ^ ApplyTransformation.txt_of_inline_macro ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") - style suri prefix + params suri in [], str, String.length parsed_text and eval_executable include_paths (buffer : GText.buffer) guistuff -lexicon_status grafite_status user_goal unparsed_text skipped_txt nonskipped_txt +grafite_status user_goal unparsed_text skipped_txt nonskipped_txt script ex loc = - let module TAPp = GrafiteAstPp in - let module MD = GrafiteDisambiguator in - let module ML = MatitaMisc in try ignore (buffer#move_mark (`NAME "beginning_of_statement") ~where:((buffer#get_iter_at_mark (`NAME "locked"))#forward_chars (Glib.Utf8.length skipped_txt))) ; eval_with_engine include_paths - guistuff lexicon_status grafite_status user_goal skipped_txt nonskipped_txt + guistuff grafite_status user_goal skipped_txt nonskipped_txt (TA.Executable (loc, ex)) with MatitaTypes.Cancel -> [], "", 0 @@ -618,22 +652,27 @@ script ex loc None -> [] | Some n -> GrafiteTypes.get_proof_context grafite_status n in let grafite_status,macro = lazy_macro context in - eval_macro include_paths buffer guistuff lexicon_status grafite_status + eval_macro include_paths buffer guistuff grafite_status user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro + | GrafiteEngine.NMacro (_loc,macro) -> + eval_nmacro include_paths buffer guistuff grafite_status + user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro + -and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status +and eval_statement include_paths (buffer : GText.buffer) guistuff grafite_status user_goal script statement = - let (lexicon_status,st), unparsed_text = + let (grafite_status,st), unparsed_text = match statement with | `Raw text -> if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; let ast = wrap_with_make include_paths - (GrafiteParser.parse_statement (Ulexing.from_utf8_string text)) lexicon_status + (GrafiteParser.parse_statement (Ulexing.from_utf8_string text)) + grafite_status in ast, text - | `Ast (st, text) -> (lexicon_status, st), text + | `Ast (st, text) -> (grafite_status, st), text in let text_of_loc floc = let nonskipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in @@ -647,23 +686,32 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status match st with | GrafiteParser.LNone loc -> let parsed_text, _, _, parsed_text_length = text_of_loc loc in - [(grafite_status,lexicon_status),parsed_text],"", + [grafite_status,parsed_text],"", parsed_text_length + | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) -> + let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in + eval_executable include_paths buffer guistuff + grafite_status user_goal unparsed_text skipped nonskipped script ex loc + | GrafiteParser.LSome (GrafiteAst.Comment (loc, GrafiteAst.Code (_, ex))) + when Helm_registry.get_bool "matita.execcomments" -> + let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in + eval_executable include_paths buffer guistuff + grafite_status user_goal unparsed_text skipped nonskipped script ex loc | GrafiteParser.LSome (GrafiteAst.Comment (loc, _)) -> let parsed_text, _, _, parsed_text_length = text_of_loc loc in let remain_len = String.length unparsed_text - parsed_text_length in let s = String.sub unparsed_text parsed_text_length remain_len in let s,text,len = try - eval_statement include_paths buffer guistuff lexicon_status + eval_statement include_paths buffer guistuff grafite_status user_goal script (`Raw s) with HExtlib.Localized (floc, exn) -> HExtlib.raise_localized_exception ~offset:(MatitaGtkMisc.utf8_string_length parsed_text) floc exn - | GrafiteDisambiguator.DisambiguationError (offset,errorll) -> + | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> raise - (GrafiteDisambiguator.DisambiguationError + (MultiPassDisambiguator.DisambiguationError (offset+parsed_text_length, errorll)) in assert (text=""); (* no macros inside comments, please! *) @@ -671,18 +719,12 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status | (statuses,text)::tl -> (statuses,parsed_text ^ text)::tl,"",parsed_text_length + len | [] -> [], "", 0) - | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) -> - let _, nonskipped, skipped, parsed_text_length = - text_of_loc loc - in - eval_executable include_paths buffer guistuff lexicon_status - grafite_status user_goal unparsed_text skipped nonskipped script ex loc let fresh_script_id = let i = ref 0 in fun () -> incr i; !i -class script ~(source_view: GSourceView.source_view) +class script ~(source_view: GSourceView2.source_view) ~(mathviewer: MatitaTypes.mathViewer) ~set_star ~ask_confirmation @@ -690,13 +732,21 @@ class script ~(source_view: GSourceView.source_view) () = let buffer = source_view#buffer in let source_buffer = source_view#source_buffer in -let initial_statuses baseuri = +let initial_statuses current baseuri = + let empty_lstatus = new LexiconEngine.status in + (match current with + Some current -> + LexiconSync.time_travel ~present:current ~past:empty_lstatus; + GrafiteSync.time_travel ~present:current (); + (* CSC: there is a known bug in invalidation; temporary fix here *) + NCicEnvironment.invalidate () + | None -> ()); let lexicon_status = - CicNotation2.load_notation ~include_paths:[] + CicNotation2.load_notation ~include_paths:[] empty_lstatus BuildTimeConf.core_notation_script in - let grafite_status = GrafiteSync.init baseuri in - grafite_status,lexicon_status + let grafite_status = GrafiteSync.init lexicon_status baseuri in + grafite_status in let read_include_paths file = try @@ -761,7 +811,7 @@ object (self) val mutable statements = [] (** executed statements *) - val mutable history = [ initial_statuses default_buri ] + val mutable history = [ initial_statuses None default_buri ] (** list of states before having executed statements. Head element of this * list is the current state, last element is the state at the beginning of * the script. @@ -785,19 +835,21 @@ object (self) (* history can't be empty, the invariant above grant that it contains at * least the init grafite_status *) - method grafite_status = match history with (s,_)::_ -> s | _ -> assert false - method lexicon_status = match history with (_,ss)::_ -> ss | _ -> assert false + method grafite_status = match history with s::_ -> s | _ -> assert false method private _advance ?statement () = let s = match statement with Some s -> s | None -> self#getFuture in if self#bos then LibraryClean.clean_baseuris [self#buri_of_current_file]; HLog.debug ("evaluating: " ^ first_line s ^ " ..."); + let time1 = Unix.gettimeofday () in let entries, newtext, parsed_len = try - eval_statement self#include_paths buffer guistuff self#lexicon_status + eval_statement self#include_paths buffer guistuff self#grafite_status userGoal self (`Raw s) with End_of_file -> raise Margin in + let time2 = Unix.gettimeofday () in + HLog.debug ("... done in " ^ string_of_float (time2 -. time1) ^ "s"); let new_statuses, new_statements = let statuses, texts = List.split entries in statuses, texts @@ -820,21 +872,21 @@ object (self) buffer#insert ~iter:(buffer#get_iter_at_mark (`MARK locked_mark)) newtext; (* here we need to set the Goal in case we are going to cursor (or to bottom) and we will face a macro *) - match self#grafite_status.proof_status with + match self#grafite_status#proof_status with Incomplete_proof p -> userGoal <- (try Some (Continuationals.Stack.find_goal p.stack) with Failure _ -> None) | _ -> userGoal <- None - method private _retract offset lexicon_status grafite_status new_statements + method private _retract offset grafite_status new_statements new_history = - let cur_grafite_status,cur_lexicon_status = + let cur_grafite_status = match history with s::_ -> s | [] -> assert false in - LexiconSync.time_travel ~present:cur_lexicon_status ~past:lexicon_status; - GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status; + LexiconSync.time_travel ~present:cur_grafite_status ~past:grafite_status; + GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status (); statements <- new_statements; history <- new_history; self#moveMark (- offset) @@ -851,7 +903,7 @@ object (self) method retract () = try - let cmp,new_statements,new_history,(grafite_status,lexicon_status) = + let cmp,new_statements,new_history,grafite_status = match statements,history with stat::statements, _::(status::_ as history) -> assert (Glib.Utf8.validate stat); @@ -859,7 +911,7 @@ object (self) | [],[_] -> raise Margin | _,_ -> assert false in - self#_retract cmp lexicon_status grafite_status new_statements + self#_retract cmp grafite_status new_statements new_history; self#notify with @@ -868,9 +920,43 @@ object (self) | exc -> self#notify; raise exc method private getFuture = - buffer#get_text ~start:(buffer#get_iter_at_mark (`MARK locked_mark)) - ~stop:buffer#end_iter () + let lock = buffer#get_iter_at_mark (`MARK locked_mark) in + let text = buffer#get_text ~start:lock ~stop:buffer#end_iter () in + text + method expandAllVirtuals = + let lock = buffer#get_iter_at_mark (`MARK locked_mark) in + let text = buffer#get_text ~start:lock ~stop:buffer#end_iter () in + buffer#delete ~start:lock ~stop:buffer#end_iter; + let text = Pcre.replace ~pat:":=" ~templ:"\\def" text in + let text = Pcre.replace ~pat:"->" ~templ:"\\to" text in + let text = Pcre.replace ~pat:"=>" ~templ:"\\Rightarrow" text in + let text = + Pcre.substitute_substrings + ~subst:(fun str -> + let pristine = Pcre.get_substring str 0 in + let input = + if pristine.[0] = ' ' then + String.sub pristine 1 (String.length pristine -1) + else pristine + in + let input = + if input.[String.length input-1] = ' ' then + String.sub input 0 (String.length input -1) + else input + in + let before, after = + if input = "\\forall" || + input = "\\lambda" || + input = "\\exists" then "","" else " ", " " + in + try + before ^ Glib.Utf8.from_unichar + (snd (Virtuals.symbol_of_virtual input)) ^ after + with Virtuals.Not_a_virtual -> pristine) + ~pat:" ?\\\\[a-zA-Z]+ ?" text + in + buffer#insert ~iter:lock text (** @param rel_offset relative offset from current position of locked_mark *) method private moveMark rel_offset = @@ -902,13 +988,12 @@ object (self) val mutable observers = [] - method addObserver (o: LexiconEngine.status -> GrafiteTypes.status -> unit) = + method addObserver (o: GrafiteTypes.status -> unit) = observers <- o :: observers method private notify = - let lexicon_status = self#lexicon_status in let grafite_status = self#grafite_status in - List.iter (fun o -> o lexicon_status grafite_status) observers + List.iter (fun o -> o grafite_status) observers method loadFromString s = buffer#set_text s; @@ -926,7 +1011,6 @@ object (self) | Some f -> Some (Librarian.absolutize f) | None -> None in - self#goto_top; filename_ <- file; include_paths_ <- (match file with Some file -> read_include_paths file | None -> []); @@ -956,22 +1040,9 @@ object (self) HLog.debug ("backup " ^ f ^ " saved") end - method private goto_top = - let grafite_status,lexicon_status = - let rec last x = function - | [] -> x - | hd::tl -> last hd tl - in - last (self#grafite_status,self#lexicon_status) history - in - (* FIXME: this is not correct since there is no undo for - * library_objects.set_default... *) - GrafiteSync.time_travel ~present:self#grafite_status ~past:grafite_status; - LexiconSync.time_travel ~present:self#lexicon_status ~past:lexicon_status - method private reset_buffer = statements <- []; - history <- [ initial_statuses self#buri_of_current_file ]; + history <- [ initial_statuses (Some self#grafite_status) self#buri_of_current_file ]; userGoal <- None; self#notify; buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter; @@ -1002,7 +1073,6 @@ object (self) match pos with | `Top -> dispose_old_locked_mark (); - self#goto_top; self#reset_buffer; self#notify | `Bottom -> @@ -1048,9 +1118,9 @@ object (self) in let rec back_until_cursor len = (* go backward until locked < cursor *) function - statements, ((grafite_status,lexicon_status)::_ as history) + statements, ((grafite_status)::_ as history) when len <= 0 -> - self#_retract (icmp - len) lexicon_status grafite_status statements + self#_retract (icmp - len) grafite_status statements history | statement::tl1, _::tl2 -> back_until_cursor (len - MatitaGtkMisc.utf8_string_length statement) (tl1,tl2) @@ -1075,7 +1145,7 @@ object (self) HLog.error "The script is too big!\n" method onGoingProof () = - match self#grafite_status.proof_status with + match self#grafite_status#proof_status with | No_proof | Proof _ -> false | Incomplete_proof _ -> true | Intermediate _ -> assert false @@ -1115,15 +1185,13 @@ object (self) let _,parsed_text_length = MatitaGtkMisc.utf8_parsed_text s loc in (* CSC: why +1 in the following lines ???? *) let parsed_text_length = parsed_text_length + 1 in -prerr_endline ("## " ^ string_of_int parsed_text_length); let remain_len = String.length s - parsed_text_length in let next = String.sub s parsed_text_length remain_len in is_there_only_comments lexicon_status next | GrafiteParser.LNone _ | GrafiteParser.LSome (GrafiteAst.Executable _) -> false in - try - is_there_only_comments self#lexicon_status self#getFuture + try is_there_only_comments self#grafite_status self#getFuture with | LexiconEngine.IncludedFileNotCompiled _ | HExtlib.Localized _