X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaScript.ml;h=157906fc8ce3eba402581ccc4c5d54133fcf21f3;hb=b890d1579e24e6f7e1d4c6af9afcb0431584a3e0;hp=a9a86bb80b557fa6629d139e54bcb09abcbcb3cc;hpb=f3d0ba1e75bc3383d766f3a33a19352db19854df;p=helm.git diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index a9a86bb80..157906fc8 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -70,8 +70,7 @@ type guistuff = { 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 guistuff grafite_status skipped_txt nonskipped_txt st = let parsed_text_length = String.length skipped_txt + String.length nonskipped_txt @@ -100,7 +99,7 @@ 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) guistuff grafite_status unparsed_text parsed_text script mac = let parsed_text_length = String.length parsed_text in match mac with | TA.Screenshot (_,name) -> @@ -168,25 +167,24 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us | 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 +grafite_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 + guistuff grafite_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 + unparsed_text (skipped_txt ^ nonskipped_txt) script macro and eval_statement include_paths (buffer : GText.buffer) guistuff - grafite_status user_goal script statement + grafite_status script statement = let st,unparsed_text = match statement with @@ -212,12 +210,12 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff | 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 + grafite_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 + grafite_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 @@ -225,7 +223,7 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff let s,text,len = try eval_statement include_paths buffer guistuff - grafite_status user_goal script (`Raw s) + grafite_status script (`Raw s) with HExtlib.Localized (floc, exn) -> HExtlib.raise_localized_exception @@ -254,14 +252,14 @@ let fresh_script_id = * "TERM" and "PATTERN", in the future other targets like "MATHMLCONTENT" may * be added *) -class script ~ask_confirmation ~urichooser () = +class script ~ask_confirmation ~urichooser ~(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:(MatitaMisc.get_gui ())#main#scriptScrolledWin#add + ~packing:parent#add_with_viewport () in let buffer = source_view#buffer in let source_buffer = source_view#source_buffer in @@ -273,24 +271,28 @@ let initial_statuses current baseuri = 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 *) + (* MATITA 1.0: there is a known bug in invalidation; temporary fix here *) NCicEnvironment.invalidate () | None -> ()); let lexicon_status = empty_lstatus in + (* MATITA 1.0: ma serve ancora fare questo back-track sul lexicon_status? *) 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 rc = - Str.split (Str.regexp " ") - (List.assoc "include_paths" (Librarian.load_root_file (root^"/root"))) + 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 - List.iter (HLog.debug) rc; rc - with Librarian.NoRootFor _ | Not_found -> [] + 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 @@ -323,7 +325,7 @@ object (self) method private curdir = try let root, _buri, _fname, _tgt = - Librarian.baseuri_of_script ~include_paths:self#include_paths + Librarian.baseuri_of_script ~include_paths:self#include_paths self#filename in root @@ -338,11 +340,16 @@ object (self) Librarian.baseuri_of_script ~include_paths:self#include_paths f in buri - with Librarian.NoRootFor _ -> default_buri + with Librarian.NoRootFor _ | Librarian.FileNotFound _ -> default_buri method filename = match filename_ with None -> default_fname | Some f -> f initializer + ignore + (source_view#source_buffer#begin_not_undoable_action (); + self#reset (); + self#template (); + source_view#source_buffer#end_not_undoable_action ()); MatitaMisc.observe_font_size (fun font_size -> source_view#misc#modify_font_by_name (sprintf "%s %d" BuildTimeConf.script_font font_size)); @@ -438,11 +445,6 @@ object (self) menu#remove (redoMenuItem :> GMenu.menu_item); MatitaGtkMisc.connect_menu_item new_redoMenuItem (fun () -> self#safe_redo))); - ignore - (source_view#source_buffer#begin_not_undoable_action (); - self#reset (); - self#template (); - source_view#source_buffer#end_not_undoable_action ()) val mutable statements = [] (** executed statements *) @@ -452,9 +454,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 @@ -690,7 +689,7 @@ object (self) let entries, newtext, parsed_len = try eval_statement self#include_paths buffer guistuff - self#grafite_status userGoal self (`Raw s) + self#grafite_status self (`Raw s) with End_of_file -> raise Margin in let time2 = Unix.gettimeofday () in @@ -714,10 +713,7 @@ 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; @@ -829,10 +825,8 @@ object (self) let grafite_status = self#grafite_status in List.iter (fun o -> o grafite_status) observers - method loadFromString s = - buffer#set_text s; - self#reset_buffer; - buffer#set_modified true + method activate = + self#notify method loadFromFile f = buffer#set_text (HExtlib.input_file f); @@ -842,24 +836,21 @@ object (self) method assignFileName file = match file with None -> - (MatitaMisc.get_gui ())#main#scriptLabel#set_text default_fname; + tab_label#set_text default_fname; filename_ <- None; include_paths_ <- []; self#reset_buffer | Some file -> let f = Librarian.absolutize file in - (MatitaMisc.get_gui ())#main#scriptLabel#set_text (Filename.basename f); + tab_label#set_text (Filename.basename f); filename_ <- Some f; include_paths_ <- read_include_paths f; - self#reset_buffer; - Sys.chdir self#curdir; - HLog.debug ("Moving to " ^ Sys.getcwd ()) + self#reset_buffer method set_star b = - let label = (MatitaMisc.get_gui ())#main#scriptLabel in - label#set_text ((if b then "*" else "") ^ Filename.basename self#filename); - label#misc#set_tooltip_text - ("URI: " ^ self#buri_of_current_file ^ "\nPATH: " ^ self#filename) + tab_label#set_text ((if b then "*" else "")^Filename.basename self#filename); + tab_label#misc#set_tooltip_text + ("URI: " ^ self#buri_of_current_file ^ "\nPATH: " ^ self#filename); method saveToFile () = if self#has_name then @@ -886,7 +877,6 @@ object (self) method private reset_buffer = statements <- []; 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; buffer#move_mark (`MARK locked_mark) ~where:buffer#start_iter @@ -902,7 +892,7 @@ object (self) let template = HExtlib.input_file BuildTimeConf.script_template in buffer#insert ~iter:(buffer#get_iter `START) template; buffer#set_modified false; - self#set_star false + self#set_star false; method goto (pos: [`Top | `Bottom | `Cursor]) () = try @@ -987,11 +977,6 @@ 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 @@ -1028,18 +1013,37 @@ object (self) HLog.debug (sprintf "%d statements:" (List.length statements)); List.iter HLog.debug statements; HLog.debug ("Current file name: " ^ self#filename); + + method has_parent (p : GObj.widget) = parent#coerce#misc#get_oid = p#misc#get_oid end -let _script = ref None +let _script = ref [] -let script ~urichooser ~ask_confirmation () +let script ~urichooser ~ask_confirmation ~parent ~tab_label () = - let s = new script ~ask_confirmation ~urichooser () in - _script := Some s; + let s = new script ~ask_confirmation ~urichooser ~parent ~tab_label () in + _script := s::!_script; s -let current () = match !_script with None -> assert false | Some s -> s +let at_page page = + let notebook = (MatitaMisc.get_gui ())#main#scriptNotebook in + let parent = notebook#get_nth_page page in + try + List.find (fun s -> s#has_parent parent) !_script + with + Not_found -> assert false +;; + +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; grafite_status: GrafiteTypes.status >) ;;