X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaScript.ml;h=de78194f0254f0592642d8b90ad40c3ccd183fde;hb=d9a1ff8259a7882caa0ffd27282838c00a34cab5;hp=1f05a8837e1e5ecf95fe548839ade424960c73a6;hpb=c3dd1837c4dfd52e2d2f0b17fbe9fdae39651fe2;p=helm.git diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index 1f05a8837..de78194f0 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -65,13 +65,7 @@ let first_line s = String.sub s 0 nl_pos with Not_found -> s -type guistuff = { - urichooser: NReference.reference list -> NReference.reference list; - ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL]; -} - -let eval_with_engine include_paths guistuff grafite_status user_goal - skipped_txt nonskipped_txt st +let eval_with_engine include_paths status skipped_txt nonskipped_txt st = let parsed_text_length = String.length skipped_txt + String.length nonskipped_txt @@ -81,7 +75,7 @@ let eval_with_engine include_paths guistuff grafite_status user_goal let enriched_history_fragment = MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:(Helm_registry.get_bool "matita.do_heavy_checks") - grafite_status (text,prefix_len,st) + status (text,prefix_len,st) in let enriched_history_fragment = List.rev enriched_history_fragment in (* really fragile *) @@ -100,11 +94,11 @@ let eval_with_engine include_paths guistuff grafite_status user_goal let pp_eager_statement_ast = GrafiteAstPp.pp_statement -let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac = +let eval_nmacro include_paths (buffer : GText.buffer) status 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 status = script#status in let _,_,menv,subst,_ = status#obj in let name = Filename.dirname (script#filename) ^ "/" ^ name in let sequents = @@ -114,7 +108,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us CicMathView.screenshot status sequents menv subst name; [status, parsed_text], "", parsed_text_length | TA.NCheck (_,t) -> - let status = script#grafite_status in + let status = script#status in let _,_,menv,subst,_ = status#obj in let ctx = match Continuationals.Stack.head_goals status#stack with @@ -123,79 +117,81 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us if tl <> [] then HLog.warn "Many goals focused. Using the context of the first one\n"; - let _, ctx, _ = NCicUtils.lookup_meta g menv in - ctx in + let ctx = try + let _, ctx, _ = NCicUtils.lookup_meta g menv in ctx + with NCicUtils.Meta_not_found _ -> + HLog.warn "Current goal is closed. Using empty context."; + [ ] + in ctx + in let m, s, status, t = GrafiteDisambiguate.disambiguate_nterm - status None ctx menv subst (parsed_text,parsed_text_length, + status `XTNone ctx menv subst (parsed_text,parsed_text_length, NotationPt.Cast (t,NotationPt.Implicit `JustOne)) (* XXX use the metasenv, if possible *) in - MatitaMathView.show_entry (`NCic (t,ctx,m,s)); + MatitaMathView.cicBrowser (Some (`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 s = NTactics.intros_tac ~names_ref [] script#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 + [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 s = NnAuto.auto_tac ~params:(None,a) ~trace_ref script#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 width = + try List.assoc "width" a + with Not_found -> "" + in + let trace = "/"^(if int_of_string depth > 1 then depth ^ " width=" ^ width else "")^" by " in let thms = match !trace_ref with - | [] -> "{}" + | [] -> "" | thms -> String.concat ", " (HExtlib.filter_map (function - | NotationPt.NRef r -> Some (NCicPp.r2s true r) + | NotationPt.NRef r -> Some (NCicPp.r2s status 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 + [s, nl ^ trace ^ thms ^ "/"], "", parsed_text_length | TA.NAutoInteractive (_, (Some _,_)) -> assert false -let rec eval_executable include_paths (buffer : GText.buffer) guistuff -grafite_status user_goal unparsed_text skipped_txt nonskipped_txt -script ex loc +let rec eval_executable include_paths (buffer : GText.buffer) +status unparsed_text skipped_txt nonskipped_txt script ex loc = 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 grafite_status user_goal skipped_txt nonskipped_txt - (TA.Executable (loc, ex)) + eval_with_engine include_paths status skipped_txt nonskipped_txt + (TA.Executable (loc, ex)) with MatitaTypes.Cancel -> [], "", 0 | GrafiteEngine.NMacro (_loc,macro) -> - eval_nmacro include_paths buffer guistuff grafite_status - user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro + eval_nmacro include_paths buffer status + unparsed_text (skipped_txt ^ nonskipped_txt) script macro -and eval_statement include_paths (buffer : GText.buffer) guistuff - grafite_status user_goal script statement +and eval_statement include_paths (buffer : GText.buffer) status script + statement = let st,unparsed_text = match statement with | `Raw text -> if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; let strm = - GrafiteParser.parsable_statement grafite_status + GrafiteParser.parsable_statement status (Ulexing.from_utf8_string text) in - let ast = MatitaEngine.get_ast grafite_status include_paths strm in + let ast = MatitaEngine.get_ast status include_paths strm in ast, text | `Ast (st, text) -> st, text in @@ -211,21 +207,20 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff match st with | 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 + eval_executable include_paths buffer status unparsed_text + skipped nonskipped script ex loc | 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 + eval_executable include_paths buffer status unparsed_text + skipped nonskipped script ex loc | 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 - grafite_status user_goal script (`Raw s) + eval_statement include_paths buffer status script (`Raw s) with HExtlib.Localized (floc, exn) -> HExtlib.raise_localized_exception @@ -254,46 +249,28 @@ let fresh_script_id = * "TERM" and "PATTERN", in the future other targets like "MATHMLCONTENT" may * be added *) -class script ~ask_confirmation ~urichooser ~(parent:GBin.scrolled_window) ~tab_label () = +class script ~(parent:GBin.scrolled_window) ~tab_label () = let source_view = GSourceView2.source_view ~auto_indent:true ~insert_spaces_instead_of_tabs:true ~tab_width:2 ~right_margin_position:80 ~show_right_margin:true ~smart_home_end:`AFTER - ~packing:parent#add_with_viewport + ~packing:parent#add () in let buffer = source_view#buffer in let source_buffer = source_view#source_buffer in let similarsymbols_tag_name = "similarsymbolos" in let similarsymbols_tag = `NAME similarsymbols_tag_name in let initial_statuses current baseuri = - let empty_lstatus = new GrafiteDisambiguate.status in + let status = new MatitaEngine.status baseuri in (match current with - Some current -> - NCicLibrary.time_travel - ((new GrafiteTypes.status current#baseuri)#set_disambiguate_db current#disambiguate_db); - (* CSC: there is a known bug in invalidation; temporary fix here *) - NCicEnvironment.invalidate () + Some current -> NCicLibrary.time_travel status; +(* + (* MATITA 1.0: there is a known bug in invalidation; temporary fix here *) + NCicEnvironment.invalidate () *) | None -> ()); - let lexicon_status = empty_lstatus in - let grafite_status = (new GrafiteTypes.status baseuri)#set_disambiguate_db lexicon_status#disambiguate_db in - grafite_status -in -let read_include_paths file = - try - let root, _buri, _fname, _tgt = - Librarian.baseuri_of_script ~include_paths:[] file in - let includes = - try - Str.split (Str.regexp " ") - (List.assoc "include_paths" (Librarian.load_root_file (root^"/root"))) - with Not_found -> [] - in - let rc = root :: includes in - List.iter (HLog.debug) rc; rc - with Librarian.NoRootFor _ | Librarian.FileNotFound _ -> - [] + status in let default_buri = "cic:/matita/tests" in let default_fname = ".unnamed.ma" in @@ -308,11 +285,6 @@ object (self) val scriptId = fresh_script_id () - val guistuff = { - urichooser = urichooser source_view; - ask_confirmation = ask_confirmation; - } - val mutable filename_ = (None : string option) method has_name = filename_ <> None @@ -455,9 +427,6 @@ object (self) * the script. * Invariant: this list length is 1 + length of statements *) - (** goal as seen by the user (i.e. metano corresponding to current tab) *) - val mutable userGoal = (None : int option) - (** text mark and tag representing locked part of a script *) val locked_mark = buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter @@ -683,7 +652,7 @@ 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 status = match history with s::_ -> s | _ -> assert false method private _advance ?statement () = let s = match statement with Some s -> s | None -> self#getFuture in @@ -692,8 +661,7 @@ object (self) let time1 = Unix.gettimeofday () in let entries, newtext, parsed_len = try - eval_statement self#include_paths buffer guistuff - self#grafite_status userGoal self (`Raw s) + eval_statement self#include_paths buffer self#status self (`Raw s) with End_of_file -> raise Margin in let time2 = Unix.gettimeofday () in @@ -717,13 +685,10 @@ object (self) end; end; self#moveMark (Glib.Utf8.length new_text); - 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 *) - userGoal <- None + buffer#insert ~iter:(buffer#get_iter_at_mark (`MARK locked_mark)) newtext - method private _retract offset grafite_status new_statements new_history = - NCicLibrary.time_travel grafite_status; + method private _retract offset status new_statements new_history = + NCicLibrary.time_travel status; statements <- new_statements; history <- new_history; self#moveMark (- offset) @@ -740,7 +705,7 @@ object (self) method retract () = try - let cmp,new_statements,new_history,grafite_status = + let cmp,new_statements,new_history,status = match statements,history with stat::statements, _::(status::_ as history) -> assert (Glib.Utf8.validate stat); @@ -748,8 +713,7 @@ object (self) | [],[_] -> raise Margin | _,_ -> assert false in - self#_retract cmp grafite_status new_statements - new_history; + self#_retract cmp status new_statements new_history; self#notify with | Margin -> self#notify @@ -816,7 +780,10 @@ object (self) buffer#move_mark mark mark_position; source_view#scroll_to_mark ~use_align:true ~xalign:1.0 ~yalign:0.1 mark; end; - while Glib.Main.pending () do ignore(Glib.Main.iteration false); done + let time0 = Unix.gettimeofday () in + GtkThread.sync (fun () -> while Glib.Main.pending () do ignore(Glib.Main.iteration false); done) (); + let time1 = Unix.gettimeofday () in + HLog.debug ("... refresh done in " ^ string_of_float (time1 -. time0) ^ "s") method clean_dirty_lock = let lock_mark_iter = buffer#get_iter_at_mark (`MARK locked_mark) in @@ -829,10 +796,11 @@ object (self) observers <- o :: observers method private notify = - let grafite_status = self#grafite_status in - List.iter (fun o -> o grafite_status) observers + let status = self#status in + List.iter (fun o -> o status) observers method activate = + NCicLibrary.replace self#status; self#notify method loadFromFile f = @@ -851,7 +819,7 @@ object (self) let f = Librarian.absolutize file in tab_label#set_text (Filename.basename f); filename_ <- Some f; - include_paths_ <- read_include_paths f; + include_paths_ <- MatitaEngine.read_include_paths ~include_paths:[] f; self#reset_buffer method set_star b = @@ -873,18 +841,17 @@ object (self) method private _saveToBackupFile () = if buffer#modified then begin - let f = self#filename in + let f = self#filename ^ "~" in let oc = open_out f in output_string oc (buffer#get_text ~start:buffer#start_iter ~stop:buffer#end_iter ()); close_out oc; - HLog.debug ("backup " ^ f ^ " saved") + HLog.debug ("backup " ^ f ^ " saved") end method private reset_buffer = statements <- []; - history <- [ initial_statuses (Some self#grafite_status) self#buri_of_current_file ]; - userGoal <- None; + history <- [ initial_statuses (Some self#status) self#buri_of_current_file ]; self#notify; buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter; buffer#move_mark (`MARK locked_mark) ~where:buffer#start_iter @@ -959,9 +926,9 @@ object (self) in let rec back_until_cursor len = (* go backward until locked < cursor *) function - statements, ((grafite_status)::_ as history) + statements, ((status)::_ as history) when len <= 0 -> - self#_retract (icmp - len) grafite_status statements + self#_retract (icmp - len) status statements history | statement::tl1, _::tl2 -> back_until_cursor (len - MatitaGtkMisc.utf8_string_length statement) (tl1,tl2) @@ -985,33 +952,28 @@ object (self) with Invalid_argument "Array.make" -> HLog.error "The script is too big!\n" - method stack = (assert false : Continuationals.Stack.t) (* MATITA 1.0 GrafiteTypes.get_stack - self#grafite_status *) - method setGoal n = userGoal <- n - method goal = userGoal - method bos = match history with | _::[] -> true | _ -> false method eos = - let rec is_there_only_comments lexicon_status s = + let rec is_there_only_comments status s = if Pcre.pmatch ~rex:only_dust_RE s then raise Margin; let strm = - GrafiteParser.parsable_statement lexicon_status + GrafiteParser.parsable_statement status (Ulexing.from_utf8_string s)in - match GrafiteParser.parse_statement lexicon_status strm with + match GrafiteParser.parse_statement status strm with | GrafiteAst.Comment (loc,_) -> 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 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 + is_there_only_comments status next | GrafiteAst.Executable _ -> false in - try is_there_only_comments self#grafite_status self#getFuture + try is_there_only_comments self#status self#getFuture with | NCicLibrary.IncludedFileNotCompiled _ | HExtlib.Localized _ @@ -1032,9 +994,9 @@ end let _script = ref [] -let script ~urichooser ~ask_confirmation ~parent ~tab_label () +let script ~parent ~tab_label () = - let s = new script ~ask_confirmation ~urichooser ~parent ~tab_label () in + let s = new script ~parent ~tab_label () in _script := s::!_script; s @@ -1050,8 +1012,13 @@ let at_page page = let current () = at_page ((MatitaMisc.get_gui ())#main#scriptNotebook#current_page) +let destroy page = + let s = at_page page in + _script := List.filter ((<>) s) !_script +;; + let iter_scripts f = List.iter f !_script;; let _ = - CicMathView.register_matita_script_current (current :> unit -> < advance: ?statement:string -> unit -> unit; grafite_status: GrafiteTypes.status; setGoal: int option -> unit >) + CicMathView.register_matita_script_current (current :> unit -> < advance: ?statement:string -> unit -> unit; status: GrafiteTypes.status >) ;;