From: Enrico Tassi Date: Fri, 15 Jul 2005 16:50:12 +0000 (+0000) Subject: matitamake is integrated with matita X-Git-Tag: pre_notation~6 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=619a3a478a4f6b0a50782b620009f6a141c30a53;p=helm.git matitamake is integrated with matita (but currently compiles on stdout) --- diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index c0b49433e..a3a6fe77d 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -33,6 +33,7 @@ CMOS = \ matitaDisambiguator.cmo \ matitaEngine.cmo \ matitacLib.cmo \ + matitamakeLib.cmo \ matitaScript.cmo \ matitaGeneratedGui.cmo \ matitaGtkMisc.cmo \ diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 1f035a0fa..68fecc5b5 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -881,7 +881,7 @@ Copyright (C) 2005, True - + True gtk-new 1 @@ -902,7 +902,7 @@ Copyright (C) 2005, - + True gtk-open 1 @@ -923,7 +923,7 @@ Copyright (C) 2005, - + True gtk-save 1 @@ -943,7 +943,7 @@ Copyright (C) 2005, True - + True gtk-save-as 1 @@ -957,7 +957,28 @@ Copyright (C) 2005, - + + True + _Developments... + True + + + + + True + gtk-execute + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + True @@ -970,7 +991,7 @@ Copyright (C) 2005, - + True gtk-quit 1 @@ -1004,7 +1025,7 @@ Copyright (C) 2005, - + True gtk-find-and-replace 1 @@ -3029,4 +3050,521 @@ Copyright (C) 2005, + + Create development + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_CENTER_ALWAYS + True + False + False + True + False + False + GDK_WINDOW_TYPE_HINT_UTILITY + GDK_GRAVITY_NORTH_WEST + + + + True + False + 0 + + + + 3 + True + 2 + 3 + False + 5 + 5 + + + + True + Name + False + False + GTK_JUSTIFY_LEFT + False + False + 0 + 0.5 + 0 + 0 + + + 0 + 1 + 0 + 1 + fill + + + + + + + True + Root directory + False + False + GTK_JUSTIFY_LEFT + False + False + 0 + 0.5 + 0 + 0 + + + 0 + 1 + 1 + 2 + fill + + + + + + + True + True + True + True + 0 + + True + * + False + + + 1 + 2 + 0 + 1 + + + + + + + True + True + True + True + 0 + + True + * + False + + + 1 + 2 + 1 + 2 + + + + + + + True + True + ... + True + GTK_RELIEF_NORMAL + True + + + 2 + 3 + 1 + 2 + fill + + + + + + 0 + False + True + + + + + + True + + + 2 + False + True + + + + + + 3 + True + False + 5 + + + + True + False + 0 + + + + + + + + + + + 0 + True + True + + + + + + True + True + gtk-add + True + GTK_RELIEF_NORMAL + True + + + 0 + False + False + + + + + + True + True + gtk-cancel + True + GTK_RELIEF_NORMAL + True + + + 0 + False + False + + + + + 0 + False + True + + + + + + + + Developments + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_CENTER + False + True + False + True + False + False + GDK_WINDOW_TYPE_HINT_NORMAL + GDK_GRAVITY_NORTH_WEST + + + + True + False + 0 + + + + True + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_IN + GTK_CORNER_TOP_LEFT + + + + True + True + False + False + False + True + + + + + 0 + True + True + + + + + + True + + + 2 + False + True + + + + + + 3 + True + False + 4 + + + + True + False + 0 + + + + + + + + + + + 0 + True + True + + + + + + True + True + gtk-new + True + GTK_RELIEF_NORMAL + True + + + 0 + False + False + + + + + + True + True + gtk-delete + True + GTK_RELIEF_NORMAL + True + + + 0 + False + False + + + + + + True + True + GTK_RELIEF_NORMAL + True + + + + True + 0.5 + 0.5 + 0 + 0 + 0 + 0 + 0 + 0 + + + + True + False + 2 + + + + True + gtk-execute + 4 + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + _Build + True + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + + + + 0 + False + False + + + + + + True + True + GTK_RELIEF_NORMAL + True + + + + True + 0.5 + 0.5 + 0 + 0 + 0 + 0 + 0 + 0 + + + + True + False + 2 + + + + True + gtk-clear + 4 + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + C_lean + True + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + + + + 0 + False + False + + + + + + True + True + gtk-close + True + GTK_RELIEF_NORMAL + True + + + 0 + False + False + + + + + 0 + False + True + + + + + + diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index ade151a69..4e225e03b 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -36,6 +36,7 @@ let _ = Http_getter.init (); MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); MatitaDb.create_owner_environment (); + MatitamakeLib.initialize (); GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *) ignore (GMain.Main.init ()); @@ -90,6 +91,7 @@ let script = (fun ~title ~message -> MatitaGtkMisc.ask_confirmation ~title ~message ~parent:gui#main#toplevel ()) + ~develcreator:gui#createDevelopment () (* math viewers *) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index c3a8be67d..cf83195dc 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -3,6 +3,7 @@ open Printf open MatitaTypes exception Drop;; +exception UnableToInclude of string;; let debug = false ;; let debug_print = if debug then prerr_endline else ignore ;; @@ -458,6 +459,7 @@ let try_open_in paths path = with Sys_error _ as exc -> MatitaLog.error ("Unable to read " ^ path); MatitaLog.error ("opts.include_paths was " ^ String.concat ":" paths); + MatitaLog.error ("current working directory is " ^ Unix.getcwd ()); raise exc ;; @@ -470,7 +472,11 @@ let eval_command opts status cmd = (TacticAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev} | TacticAst.Include (loc, path) -> let path = MatitaMisc.obj_file_of_script path in - let stream = Stream.of_channel (try_open_in opts.include_paths path) in + let stream = + try + Stream.of_channel (try_open_in opts.include_paths path) + with Sys_error _ -> raise (UnableToInclude path) + in let status = ref status in !eval_from_stream_ref status stream (fun _ _ -> ()); !status diff --git a/helm/matita/matitaEngine.mli b/helm/matita/matitaEngine.mli index f9699fbb5..7ceb965e9 100644 --- a/helm/matita/matitaEngine.mli +++ b/helm/matita/matitaEngine.mli @@ -24,6 +24,7 @@ *) exception Drop +exception UnableToInclude of string (* heavy checks slow down the compilation process but give you some interesting * infos like if the theorem is a duplicate *) diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml index 8a7048bbd..686f54399 100644 --- a/helm/matita/matitaGtkMisc.ml +++ b/helm/matita/matitaGtkMisc.ml @@ -83,35 +83,89 @@ let add_key_binding key callback (evbox: GBin.event_box) = false | _ -> false)) -class stringListModel (tree_view: GTree.view) = +class multiStringListModel ~cols (tree_view: GTree.view) = let column_list = new GTree.column_list in - let text_column = column_list#add Gobject.Data.string in + let text_columns = + let rec aux = function + | 0 -> [] + | n -> column_list#add Gobject.Data.string :: aux (n - 1) + in + aux cols + in let list_store = GTree.list_store column_list in - let renderer = (GTree.cell_renderer_text [], ["text", text_column]) in - let view_column = GTree.view_column ~renderer () in + let renderers = + List.map + (fun text_column -> + (GTree.cell_renderer_text [], ["text", text_column])) + text_columns + in + let view_columns = + List.map + (fun renderer -> GTree.view_column ~renderer ()) + renderers + in object (self) + val text_columns = text_columns + initializer tree_view#set_model (Some (list_store :> GTree.model)); - ignore (tree_view#append_column view_column) + List.iter + (fun view_column -> ignore (tree_view#append_column view_column)) + view_columns method list_store = list_store - method easy_append s = + method easy_mappend slist = let tree_iter = list_store#append () in - list_store#set ~row:tree_iter ~column:text_column s + List.iter2 + (fun s text_column -> + list_store#set ~row:tree_iter ~column:text_column s) + slist text_columns - method easy_insert pos s = + method easy_minsert pos s = let tree_iter = list_store#insert pos in - list_store#set ~row:tree_iter ~column:text_column s + List.iter2 + (fun s text_column -> + list_store#set ~row:tree_iter ~column:text_column s) + s text_columns - method easy_selection () = + method easy_mselection () = List.map (fun tree_path -> let iter = list_store#get_iter tree_path in - list_store#get ~row:iter ~column:text_column) + List.map + (fun text_column -> + list_store#get ~row:iter ~column:text_column) + text_columns) + tree_view#selection#get_selected_rows + end + +class stringListModel (tree_view: GTree.view) = + object (self) + inherit multiStringListModel ~cols:1 tree_view as multi + + method list_store = multi#list_store + + method easy_append s = + multi#easy_mappend [s] + + method easy_insert pos s = + multi#easy_minsert pos [s] + + method easy_selection () = + let m = List.map + (fun tree_path -> + let iter = self#list_store#get_iter tree_path in + List.map + (fun text_column -> + self#list_store#get ~row:iter ~column:text_column) + text_columns) tree_view#selection#get_selected_rows + in + List.map (function [x] -> x | _ -> assert false) m end + class taggedStringListModel ~(tags:(string * GdkPixbuf.pixbuf) list) (tree_view: GTree.view) = diff --git a/helm/matita/matitaGtkMisc.mli b/helm/matita/matitaGtkMisc.mli index 7d4e28955..91a3e495b 100644 --- a/helm/matita/matitaGtkMisc.mli +++ b/helm/matita/matitaGtkMisc.mli @@ -70,16 +70,29 @@ val connect_key: (unit -> unit) -> (* callback *) unit + (** n-ary string column list *) +class multiStringListModel: + cols:int -> + GTree.view -> + object + method list_store: GTree.list_store (** list_store forwarding *) + + method easy_mappend: string list -> unit (** append + set *) + method easy_minsert: int -> string list -> unit (** insert + set *) + method easy_mselection: unit -> string list list + end + (** single string column list *) class stringListModel: GTree.view -> object - method list_store: GTree.list_store (** list_store forwarding *) + inherit multiStringListModel method easy_append: string -> unit (** append + set *) method easy_insert: int -> string -> unit (** insert + set *) method easy_selection: unit -> string list end + (** as above with Pixbuf associated to each row. Each time an insert is * performed a string tag should be specified, the corresponding pixbuf in the diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 652c720b9..51b17451e 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -110,6 +110,8 @@ class gui () = let about = new aboutWin () in let fileSel = new fileSelectionWin () in let findRepl = new findReplWin () in + let develList = new develListWin () in + let newDevel = new newDevelopmentWin () in let keyBindingBoxes = (* event boxes which should receive global key events *) [ main#mainWinEventBox ] in @@ -131,8 +133,10 @@ class gui () = object (self) val mutable chosen_file = None val mutable _ok_not_exists = false + val mutable _only_directory = false val mutable script_fname = None val mutable font_size = default_font_size + val mutable next_devel_must_contain = None initializer (* glade's check widgets *) @@ -195,6 +199,94 @@ class gui () = ignore(self#main#findReplMenuItem#connect#activate ~callback:show_find_Repl); ignore (findRepl#findEntry#connect#activate ~callback:find_forward); + (* developments win *) + let model = + new MatitaGtkMisc.multiStringListModel + ~cols:2 develList#developmentsTreeview + in + let refresh_devels_win () = + model#list_store#clear (); + List.iter + (fun (name, root) -> model#easy_mappend [name;root]) + (MatitamakeLib.list_known_developments ()) + in + let get_devel_selected () = + match model#easy_mselection () with + | [[name;_]] -> MatitamakeLib.development_for_name name + | _ -> assert false + in + connect_button develList#newButton + (fun () -> + next_devel_must_contain <- None; + newDevel#toplevel#misc#show()); + connect_button develList#deleteButton + (fun () -> + (match get_devel_selected () with + | None -> () + | Some d -> MatitamakeLib.destroy_development d); + refresh_devels_win ()); + connect_button develList#buildButton + (fun () -> + match get_devel_selected () with + | None -> () + | Some d -> ignore(MatitamakeLib.build_development d)); + connect_button develList#cleanButton + (fun () -> + match get_devel_selected () with + | None -> () + | Some d -> ignore(MatitamakeLib.clean_development d)); + connect_button develList#closeButton + (fun () -> develList#toplevel#misc#hide()); + ignore(develList#toplevel#event#connect#delete + (fun _ -> develList#toplevel#misc#hide();true)); + let selected_devel = ref None in + connect_menu_item self#main#developmentsMenuItem + (fun () -> refresh_devels_win ();develList#toplevel#misc#show ()); + + (* add development win *) + let check_if_root_contains root = + match next_devel_must_contain with + | None -> true + | Some path -> + let is_prefix_of d1 d2 = + let len1 = String.length d1 in + let len2 = String.length d2 in + if len2 < len1 then + false + else + let pref = String.sub d2 0 len1 in + pref = d1 + in + is_prefix_of root path + in + connect_button newDevel#addButton + (fun () -> + let name = newDevel#nameEntry#text in + let root = newDevel#rootEntry#text in + if check_if_root_contains root then + begin + ignore (MatitamakeLib.initialize_development name root); + refresh_devels_win (); + newDevel#nameEntry#set_text ""; + newDevel#rootEntry#set_text ""; + newDevel#toplevel#misc#hide() + end + else + MatitaLog.error ("The selected root does not contain " ^ + match next_devel_must_contain with + | Some x -> x + | _ -> assert false)); + connect_button newDevel#chooseRootButton + (fun () -> + let path = self#chooseDir () in + match path with + | Some path -> newDevel#rootEntry#set_text path + | None -> ()); + connect_button newDevel#cancelButton + (fun () -> newDevel#toplevel#misc#hide ()); + ignore(newDevel#toplevel#event#connect#delete + (fun _ -> newDevel#toplevel#misc#hide();true)); + (* file selection win *) ignore (fileSel#fileSelectionWin#event#connect#delete (fun _ -> true)); ignore (fileSel#fileSelectionWin#connect#response (fun event -> @@ -207,9 +299,17 @@ class gui () = | `OK -> let fname = fileSel#fileSelectionWin#filename in if Sys.file_exists fname then - (if is_regular fname then return (Some fname)) + begin + if is_regular fname && not(_only_directory) then + return (Some fname) + else if _only_directory && is_dir fname then + return (Some fname) + end else - (if _ok_not_exists then return (Some fname)) + begin + if _ok_not_exists then + return (Some fname) + end | `CANCEL -> return None | `HELP -> () | `DELETE_EVENT -> return None)); @@ -218,7 +318,7 @@ class gui () = main#helpMenu#set_right_justified true; (* console *) let adj = main#logScrolledWin#vadjustment in - ignore (adj#connect#changed + ignore (adj#connect#changed (fun _ -> adj#set_value (adj#upper -. adj#page_size))); console#message (sprintf "\tMatita version %s\n" BuildTimeConf.version); (* toolbar *) @@ -478,6 +578,8 @@ class gui () = method fileSel = fileSel method findRepl = findRepl method main = main + method develList = develList + method newDevel = newDevel method newBrowserWin () = object (self) @@ -523,9 +625,22 @@ class gui () = method chooseFile ?(ok_not_exists = false) () = _ok_not_exists <- ok_not_exists; + _only_directory <- false; + fileSel#fileSelectionWin#show (); + GtkThread.main (); + chosen_file + + method private chooseDir ?(ok_not_exists = false) () = + _ok_not_exists <- ok_not_exists; + _only_directory <- true; fileSel#fileSelectionWin#show (); GtkThread.main (); + (* we should check that this is a directory *) chosen_file + + method createDevelopment ~containing = + next_devel_must_contain <- containing; + newDevel#toplevel#misc#show() method askText ?(title = "") ?(msg = "") () = let dialog = new textDialog () in diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli index 6f9601f71..550d86c60 100644 --- a/helm/matita/matitaGui.mli +++ b/helm/matita/matitaGui.mli @@ -52,6 +52,8 @@ object method fileSel : MatitaGeneratedGui.fileSelectionWin method main : MatitaGeneratedGui.mainWin method findRepl : MatitaGeneratedGui.findReplWin + method develList: MatitaGeneratedGui.develListWin + method newDevel: MatitaGeneratedGui.newDevelopmentWin (* method toolbar : MatitaGeneratedGui.toolBarWin *) method console: console @@ -73,6 +75,7 @@ object * @param ok_not_exists if set to true returns also non existent files * (useful for save). Defaults to false *) method chooseFile: ?ok_not_exists:bool -> unit -> string option + method createDevelopment: containing:string option -> unit (** prompt the user for a (multiline) text entry *) method askText: ?title:string -> ?msg:string -> unit -> string option diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index 53d7bd317..c0277ea46 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -51,6 +51,10 @@ let output_file data file = output_string oc data; close_out oc + +let absolute_path file = + if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file + let is_proof_script fname = true (** TODO Zack *) let is_proof_object fname = true (** TODO Zack *) diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli index 5ea5c4394..eb6e451c7 100644 --- a/helm/matita/matitaMisc.mli +++ b/helm/matita/matitaMisc.mli @@ -32,6 +32,8 @@ val is_regular: string -> bool (** @return true if file is a regular file *) val input_file: string -> string (** read all the contents of file to string *) val output_file: string -> string -> unit (** write string to file *) +val absolute_path: string -> string + (** @return true if file is a (textual) proof script *) val is_proof_script: string -> bool diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index b077021e3..4f6627fcd 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -65,9 +65,26 @@ let goal_ast n = let loc = CicAst.dummy_floc in A.Executable (loc, A.Tactical (loc, A.Tactic (loc, A.Goal (loc, n)))) -let eval_with_engine status user_goal parsed_text st = +type guistuff = { + mathviewer:MatitaTypes.mathViewer; + urichooser: UriManager.uri list -> UriManager.uri list; + ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL]; + develcreator: containing:string option -> unit; + mutable filenamedata: string option * MatitamakeLib.development option +} + +let eval_with_engine guistuff status user_goal parsed_text st = let module TA = TacticAst in let module TAPp = TacticAstPp in + let include_ = + match guistuff.filenamedata with + | _,None -> [] + | None,Some devel -> [MatitamakeLib.root_for_development devel ] + | Some f,_ -> + match MatitamakeLib.development_for_dir (Filename.dirname f) with + | None -> [] + | Some devel -> [MatitamakeLib.root_for_development devel ] + in let parsed_text_length = String.length parsed_text in let loc, ex = match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false @@ -77,11 +94,14 @@ let eval_with_engine status user_goal parsed_text st = match status.proof_status with | Incomplete_proof (_, goal) when goal <> user_goal -> goal_changed := true; - MatitaEngine.eval_ast + MatitaEngine.eval_ast ~include_paths:include_ ~do_heavy_checks:true status (goal_ast user_goal) | _ -> status in - let new_status = MatitaEngine.eval_ast ~do_heavy_checks:true status st in + let new_status = + MatitaEngine.eval_ast + ~include_paths:include_ ~do_heavy_checks:true status st + in let new_aliases = match ex with | TA.Command (_, TA.Alias _) @@ -123,6 +143,58 @@ let eval_with_engine status user_goal parsed_text st = in [ new_status, new_text ], parsed_text_length +let eval_with_engine guistuff status user_goal parsed_text st = + try + eval_with_engine guistuff status user_goal parsed_text st + with + MatitaEngine.UnableToInclude what as exc -> + let compile_needed_and_go_on d = + let root = MatitamakeLib.root_for_development d in + let target = root ^ "/" ^ what in + if not(MatitamakeLib.build_development ~target d) then + raise exc + else + eval_with_engine guistuff status user_goal parsed_text st + in + let do_nothing () = [], 0 in + let handle_with_devel d = + let name = MatitamakeLib.name_for_development d in + let title = "Unable to include " ^ what in + let message = + what ^ " is handled by development " ^ name ^ ".\n\n" ^ + "Should I compile it and Its dependencies?" + in + (match guistuff.ask_confirmation ~title ~message with + | `YES -> compile_needed_and_go_on d + | `NO -> raise exc + | `CANCEL -> do_nothing ()) + in + let handle_withoud_devel filename = + let title = "Unable to include " ^ what in + let message = + what ^ " is not handled by a development.\n" ^ + "All dependencies are authomatically solved for a development.\n\n" ^ + "Do you want to set up a development?" + in + (match guistuff.ask_confirmation ~title ~message with + | `YES -> + (match filename with + | Some f -> + guistuff.develcreator ~containing:(Some (Filename.dirname f)) + | None -> guistuff.develcreator ~containing:None); + do_nothing () + | `NO -> raise exc + | `CANCEL -> do_nothing()) + in + match guistuff.filenamedata with + | None,None -> handle_withoud_devel None + | None,Some d -> handle_with_devel d + | Some f,_ -> + match MatitamakeLib.development_for_dir (Filename.dirname f) with + | None -> handle_withoud_devel (Some f) + | Some d -> handle_with_devel d +;; + let disambiguate term status = let module MD = MatitaDisambiguator in let dbd = MatitaDb.instance () in @@ -134,8 +206,7 @@ let disambiguate term status = | [_,_,x,_] -> x | _ -> assert false -let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser - parsed_text script mac +let eval_macro guistuff status parsed_text script mac = let module TA = TacticAst in let module TAPp = TacticAstPp in @@ -153,18 +224,18 @@ let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser let term = disambiguate term status in let l = MQ.match_term ~dbd term in let entry = `Whelp (TAPp.pp_macro_cic (TA.WMatch (loc, term)), l) in - mathviewer#show_uri_list ~reuse:true ~entry l; + guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], parsed_text_length | TA.WInstance (loc, term) -> let term = disambiguate term status in let l = MQ.instance ~dbd term in let entry = `Whelp (TAPp.pp_macro_cic (TA.WInstance (loc, term)), l) in - mathviewer#show_uri_list ~reuse:true ~entry l; + guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], parsed_text_length | TA.WLocate (loc, s) -> let l = MQ.locate ~dbd s in let entry = `Whelp (TAPp.pp_macro_cic (TA.WLocate (loc, s)), l) in - mathviewer#show_uri_list ~reuse:true ~entry l; + guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], parsed_text_length | TA.WElim (loc, term) -> let term = disambiguate term status in @@ -175,20 +246,20 @@ let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser in let l = MQ.elim ~dbd uri in let entry = `Whelp (TAPp.pp_macro_cic (TA.WElim (loc, term)), l) in - mathviewer#show_uri_list ~reuse:true ~entry l; + guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], parsed_text_length | TA.WHint (loc, term) -> let term = disambiguate term status in let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in let l = List.map fst (MQ.experimental_hint ~dbd s) in let entry = `Whelp (TAPp.pp_macro_cic (TA.WHint (loc, term)), l) in - mathviewer#show_uri_list ~reuse:true ~entry l; + guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], parsed_text_length (* REAL macro *) | TA.Hint loc -> let s = MatitaMisc.get_proof_status status in let l = List.map fst (MQ.experimental_hint ~dbd s) in - let selected = urichooser l in + let selected = guistuff.urichooser l in (match selected with | [] -> [], parsed_text_length | [uri] -> @@ -226,7 +297,7 @@ let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser in let ty,_ = CTC.type_of_aux' metasenv context term ugraph in let t_and_ty = Cic.Cast (term,ty) in - mathviewer#show_entry (`Cic (t_and_ty,metasenv)); + guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv)); [], parsed_text_length (* | TA.Abort _ -> let rec go_back () = @@ -251,8 +322,7 @@ let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser | TA.Search_term (_, search_kind, term) -> failwith "not implemented" -let eval_executable status (mathviewer:MatitaTypes.mathViewer) urichooser -ask_confirmation user_goal parsed_text script ex = +let eval_executable guistuff status user_goal parsed_text script ex = let module TA = TacticAst in let module TAPp = TacticAstPp in let module MD = MatitaDisambiguator in @@ -266,7 +336,7 @@ ask_confirmation user_goal parsed_text script ex = | Some u -> if not (MatitacleanLib.is_empty u) then match - ask_confirmation + guistuff.ask_confirmation ~title:"Baseuri redefinition" ~message:( "Baseuri " ^ u ^ " already exists.\n" ^ @@ -276,13 +346,13 @@ ask_confirmation user_goal parsed_text script ex = | `YES -> MatitacleanLib.clean_baseuris [u] | `NO -> () | `CANCEL -> raise MatitaTypes.Cancel); - eval_with_engine status user_goal parsed_text (TA.Executable (loc, ex)) + eval_with_engine + guistuff status user_goal parsed_text (TA.Executable (loc, ex)) with MatitaTypes.Cancel -> [], 0) | TA.Macro (_,mac) -> - eval_macro status mathviewer urichooser parsed_text script mac + eval_macro guistuff status parsed_text script mac -let rec eval_statement status (mathviewer:MatitaTypes.mathViewer) urichooser -ask_confirmation user_goal script s = +let rec eval_statement guistuff status user_goal script s = if Pcre.pmatch ~rex:only_dust_RE s then raise Margin; let st = CicTextualParser2.parse_statement (Stream.of_string s) in let text_of_loc loc = @@ -296,8 +366,7 @@ ask_confirmation user_goal script s = let remain_len = String.length s - parsed_text_length in let s = String.sub s parsed_text_length remain_len in let s,len = - eval_statement status - mathviewer urichooser ask_confirmation user_goal script s + eval_statement guistuff status user_goal script s in (match s with | (status, text) :: tl -> @@ -305,9 +374,7 @@ ask_confirmation user_goal script s = | [] -> [], 0) | TacticAst.Executable (loc, ex) -> let parsed_text, parsed_text_length = text_of_loc loc in - eval_executable - status mathviewer urichooser ask_confirmation - user_goal parsed_text script ex + eval_executable guistuff status user_goal parsed_text script ex let fresh_script_id = let i = ref 0 in @@ -317,14 +384,26 @@ class script ~(buffer: GText.buffer) ~(init: MatitaTypes.status) ~(mathviewer: MatitaTypes.mathViewer) ~set_star ~ask_confirmation - ~urichooser () = + ~urichooser + ~develcreator + () = object (self) - val mutable filename = None val scriptId = fresh_script_id () + + val guistuff = { + mathviewer = mathviewer; + urichooser = urichooser; + ask_confirmation = ask_confirmation; + develcreator = develcreator; + filenamedata = (None, None)} + method private getFilename = - match filename with Some f -> f | _ -> assert false + match guistuff.filenamedata with Some f,_ -> f | _ -> assert false + method private ppFilename = - match filename with Some f -> f | None -> sprintf ".unnamed%d.ma" scriptId + match guistuff.filenamedata with + | Some f,_ -> f + | None,_ -> sprintf ".unnamed%d.ma" scriptId initializer ignore(GMain.Timeout.add ~ms:300000 @@ -360,8 +439,7 @@ object (self) let s = match statement with Some s -> s | None -> self#getFuture in MatitaLog.debug ("evaluating: " ^ first_line s ^ " ..."); let (entries, parsed_len) = - eval_statement self#status - mathviewer urichooser ask_confirmation userGoal self s + eval_statement guistuff self#status userGoal self s in let (new_statuses, new_statements) = List.split entries in (* @@ -455,7 +533,9 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; buffer#set_modified false method assignFileName file = - filename <- Some file; + let abspath = MatitaMisc.absolute_path file in + let devel = MatitamakeLib.development_for_dir (Filename.dirname abspath) in + guistuff.filenamedata <- Some abspath, devel method saveToFile () = let oc = open_out self#getFilename in @@ -492,7 +572,8 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; method template () = let template = MatitaMisc.input_file BuildTimeConf.script_template in buffer#insert ~iter:(buffer#get_iter `START) template; - filename <- None; + guistuff.filenamedata <- + (None,MatitamakeLib.development_for_dir (Unix.getcwd ())); buffer#set_modified false; set_star self#ppFilename false @@ -581,16 +662,18 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; MatitaLog.debug (sprintf "%d statements:" (List.length statements)); List.iter MatitaLog.debug statements; MatitaLog.debug ("Current file name: " ^ - (match filename with None -> "[ no name ]" | Some f -> f)); + (match guistuff.filenamedata with + |None,_ -> "[ no name ]" + | Some f,_ -> f)); end let _script = ref None -let script ~buffer ~init ~mathviewer ~urichooser ~ask_confirmation ~set_star () +let script ~buffer ~init ~mathviewer ~urichooser ~develcreator ~ask_confirmation ~set_star () = let s = new script - ~buffer ~init ~mathviewer ~ask_confirmation ~urichooser ~set_star () + ~buffer ~init ~mathviewer ~ask_confirmation ~urichooser ~develcreator ~set_star () in _script := Some s; s diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli index ab39b9cfd..637584aa9 100644 --- a/helm/matita/matitaScript.mli +++ b/helm/matita/matitaScript.mli @@ -76,6 +76,7 @@ val script: init:MatitaTypes.status -> mathviewer: MatitaTypes.mathViewer-> urichooser: (UriManager.uri list -> UriManager.uri list) -> + develcreator: (containing:string option -> unit) -> ask_confirmation: (title:string -> message:string -> [`YES | `NO | `CANCEL]) -> set_star: (string -> bool -> unit) -> diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml index 2facdda09..512da157a 100644 --- a/helm/matita/matitamakeLib.ml +++ b/helm/matita/matitamakeLib.ml @@ -149,18 +149,22 @@ let initialize_development name dir = | None -> dump_development dev; rebuild_makefile dev; + developments := dev :: !developments; Some dev let make chdir args = let old = Unix.getcwd () in - Unix.chdir chdir; -(* prerr_endline (String.concat " " ("make"::args));*) - let rc = Unix.system (String.concat " " ("make"::args)) in - Unix.chdir old; - match rc with - | Unix.WEXITED 0 -> true - | Unix.WEXITED i -> logger `Error ("make returned " ^ string_of_int i);false - | _ -> logger `Error "make STOPPED or SIGNALED!";false + try + Unix.chdir chdir; + let rc = Unix.system (String.concat " " ("make"::args)) in + Unix.chdir old; + match rc with + | Unix.WEXITED 0 -> true + | Unix.WEXITED i -> logger `Error ("make returned " ^ string_of_int i);false + | _ -> logger `Error "make STOPPED or SIGNALED!";false + with Unix.Unix_error (_,cmd,err) -> + logger `Warning ("Unix Error: " ^ cmd ^ ": " ^ err); + false let call_make development target = rebuild_makefile development; @@ -195,7 +199,9 @@ let destroy_development development = unlink (pool () ^ development.name ^ rootfile); unlink (pool () ^ development.name ^ "/depend"); unlink (pool () ^ development.name ^ "/depend.short"); - rmdir (pool () ^ development.name) + rmdir (pool () ^ development.name); + developments := + List.filter (fun d -> d.name <> development.name) !developments in if not(clean_development development) then begin @@ -204,4 +210,6 @@ let destroy_development development = end; delete_development development - +let root_for_development development = development.root +let name_for_development development = development.name + diff --git a/helm/matita/matitamakeLib.mli b/helm/matita/matitamakeLib.mli index 707122668..4addbbf2b 100644 --- a/helm/matita/matitamakeLib.mli +++ b/helm/matita/matitamakeLib.mli @@ -42,5 +42,8 @@ val list_known_developments: unit -> (string * string ) list val destroy_development: development -> unit (* initiale internal data structures *) val initialize : unit -> unit - +(* gives back the root *) +val root_for_development : development -> string +(* gives back the name *) +val name_for_development : development -> string