X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaScript.ml;h=de78194f0254f0592642d8b90ad40c3ccd183fde;hb=d9a1ff8259a7882caa0ffd27282838c00a34cab5;hp=b54d2501c321bfe6ebc9d163ab742ebb88468556;hpb=3a3199faa15b1d96f8ccd8bd1551f6f4f9aceb66;p=helm.git diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index b54d2501c..de78194f0 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -65,12 +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 status 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 @@ -99,7 +94,7 @@ let eval_with_engine include_paths guistuff status skipped_txt nonskipped_txt st let pp_eager_statement_ast = GrafiteAstPp.pp_statement -let eval_nmacro include_paths (buffer : GText.buffer) guistuff status 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) -> @@ -122,22 +117,27 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff status unparsed_t 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#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#status in @@ -145,39 +145,43 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff status unparsed_t 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 +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 status skipped_txt nonskipped_txt + 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 status + eval_nmacro include_paths buffer status unparsed_text (skipped_txt ^ nonskipped_txt) script macro -and eval_statement include_paths (buffer : GText.buffer) guistuff status script +and eval_statement include_paths (buffer : GText.buffer) status script statement = let st,unparsed_text = @@ -203,12 +207,12 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff status script match st with | GrafiteAst.Executable (loc, ex) -> let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in - eval_executable include_paths buffer guistuff status unparsed_text + 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 status unparsed_text + 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 @@ -216,7 +220,7 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff status script let s = String.sub unparsed_text parsed_text_length remain_len in let s,text,len = try - eval_statement include_paths buffer guistuff status script (`Raw s) + eval_statement include_paths buffer status script (`Raw s) with HExtlib.Localized (floc, exn) -> HExtlib.raise_localized_exception @@ -245,45 +249,29 @@ 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 status = new GrafiteTypes.status baseuri in + let status = new MatitaEngine.status baseuri in (match current with - Some current -> - NCicLibrary.time_travel status; + Some current -> NCicLibrary.time_travel status; (* (* MATITA 1.0: there is a known bug in invalidation; temporary fix here *) NCicEnvironment.invalidate () *) | None -> ()); 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 _ -> - [] -in let default_buri = "cic:/matita/tests" in let default_fname = ".unnamed.ma" in object (self) @@ -297,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 @@ -678,7 +661,7 @@ object (self) let time1 = Unix.gettimeofday () in let entries, newtext, parsed_len = try - eval_statement self#include_paths buffer guistuff self#status 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 @@ -797,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 @@ -814,6 +800,7 @@ object (self) List.iter (fun o -> o status) observers method activate = + NCicLibrary.replace self#status; self#notify method loadFromFile f = @@ -832,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 = @@ -854,12 +841,12 @@ 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 = @@ -1007,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