X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaScript.ml;h=fafd7cdb2c0fc237673f313419fc8e020c43cd5e;hb=90f0070a8b639b622501bfff36e3e44853f34042;hp=b54d2501c321bfe6ebc9d163ab742ebb88468556;hpb=3a3199faa15b1d96f8ccd8bd1551f6f4f9aceb66;p=helm.git diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index b54d2501c..fafd7cdb2 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) -> @@ -130,7 +125,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff status unparsed_t 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 @@ -152,7 +147,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff status unparsed_t | 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 @@ -161,23 +156,23 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff status unparsed_t [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 +198,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 +211,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,7 +240,7 @@ 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 @@ -259,7 +254,7 @@ 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; @@ -297,11 +292,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 +668,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 @@ -1007,9 +997,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