From bd258ecf3eae6aef4ff6b1d1dd8e1c8c2bb17677 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 7 Jan 2008 09:01:29 +0000 Subject: [PATCH] removed all Developments related stuff in glade file, added matita.includes to the default paths matita uses, nice error message when a file is not found --- components/library/librarian.ml | 23 +- components/library/librarian.mli | 7 +- matita/matita.glade | 444 ------------------------------- matita/matita.ml | 1 - matita/matitaGui.ml | 27 -- matita/matitaGuiTypes.mli | 2 - matita/matitaScript.ml | 8 +- matita/matitaScript.mli | 1 - 8 files changed, 21 insertions(+), 492 deletions(-) diff --git a/components/library/librarian.ml b/components/library/librarian.ml index 72f8c50db..9a16e814d 100644 --- a/components/library/librarian.ml +++ b/components/library/librarian.ml @@ -41,7 +41,7 @@ let load_root_file rootpath = List.map (fun l -> match Str.split (Str.regexp "=") l with - | [k;v] -> Pcre.replace ~pat:" " k, Pcre.replace ~pat:" " v + | [k;v] -> Pcre.replace ~pat:"^ *" k, Pcre.replace ~pat:" *$" v | _ -> raise (Failure ("Malformed root file: " ^ rootpath))) lines ;; @@ -70,8 +70,8 @@ let find_root_for ~include_paths file = HLog.error (rootpath ^ " sets an incorrect baseuri: " ^ buri); ensure_trailing_slash root, remove_trailing_slash uri, path with Failure "find_in" -> - HLog.error ("Unable to find: "^file^"\nPaths explored:\n"); - List.iter (fun x -> HLog.error (" - "^x^"\n")) include_paths; + HLog.error ("Unable to find: "^file^"\nPaths explored:"); + List.iter (fun x -> HLog.error (" - "^x)) include_paths; raise (NoRootFor file) ;; @@ -118,7 +118,9 @@ let load_deps_file f = begin let l = input_line ic in match Str.split (Str.regexp " ") l with - | [] -> HLog.error ("malformed deps file: " ^ f); exit 1 + | [] -> + HLog.error ("Malformed deps file: " ^ f); + raise (Failure ("Malformed deps file: " ^ f)) | he::tl -> deps := (he,tl) :: !deps end done; !deps @@ -241,7 +243,8 @@ module Make = functor (F:Format) -> struct let todo = let local, remote = List.partition - (fun (file,d) -> d<>[] || F.root_of local_options file = Some root) + (fun (file,d) -> + d<>[] || F.root_of local_options file = Some root) todo in remote @ local @@ -256,7 +259,7 @@ module Make = functor (F:Format) -> struct | Some froot -> make froot [file] | None -> - HLog.error ("No root for: "^F.string_of_source_object file); + HLog.error ("No root for: "^F.string_of_source_object file); false in if rc then (file::c,f) @@ -287,9 +290,11 @@ module Make = functor (F:Format) -> struct end let write_deps_file root deps = - let oc = open_out "depends" in - List.iter (fun (t,d) -> output_string oc (t^" "^String.concat " " d^"\n")) deps; + let oc = open_out (root ^ "/depends") in + List.iter + (fun (t,d) -> output_string oc (t^" "^String.concat " " d^"\n")) + deps; close_out oc; - HLog.message ("Generated " ^ Sys.getcwd () ^ "/depends") + HLog.message ("Generated: " ^ root ^ "/depends") ;; diff --git a/components/library/librarian.mli b/components/library/librarian.mli index 1c305c265..9d042a106 100644 --- a/components/library/librarian.mli +++ b/components/library/librarian.mli @@ -1,16 +1,15 @@ exception NoRootFor of string -val find_root: string -> string +val absolutize: string -> string +val find_root: string -> string val load_root_file: string -> (string*string) list -val absolutize: string -> string - (* baseuri_of_script ?(inc:REG[matita.includes]) fname * -> * root, buri, fullpath, rootrelativepath * sample: baseuri_of_script a.ma -> /home/pippo/devel/, cic:/matita/a, - * /home/pippo/devel/a.ma *) + * /home/pippo/devel/a.ma, a.ma *) val baseuri_of_script: include_paths:string list -> string -> string * string * string * string diff --git a/matita/matita.glade b/matita/matita.glade index 462d0c64c..0eaaaa780 100644 --- a/matita/matita.glade +++ b/matita/matita.glade @@ -2589,450 +2589,6 @@ - - Create root file - True - True - GTK_WIN_POS_CENTER_ALWAYS - GDK_WINDOW_TYPE_HINT_UTILITY - - - True - - - True - 3 - 2 - 3 - 5 - 5 - - - - - - True - True - ... - True - 0 - - - 2 - 3 - 1 - 2 - GTK_FILL - - - - - - True - True - * - - - 1 - 2 - 1 - 2 - - - - - - True - True - * - - - 1 - 2 - - - - - - True - 0 - Root directory - - - 1 - 2 - GTK_FILL - - - - - - True - 0 - Base URI - - - GTK_FILL - - - - - - False - - - - - True - - - False - 2 - 1 - - - - - True - 3 - 5 - - - True - - - - - - - - - - - True - True - gtk-add - True - 0 - - - False - False - 1 - - - - - True - True - gtk-cancel - True - 0 - - - False - False - 2 - - - - - False - 2 - - - - - - 450 400 diff --git a/matita/matita.ml b/matita/matita.ml index 198fad3c5..c559358c5 100644 --- a/matita/matita.ml +++ b/matita/matita.ml @@ -65,7 +65,6 @@ let script = (fun ~title ~message -> MatitaGtkMisc.ask_confirmation ~title ~message ~parent:gui#main#toplevel ()) - ~rootcreator:gui#createRoot () in gui#sourceView#source_buffer#begin_not_undoable_action (); diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml index b2f509b25..aae91697a 100644 --- a/matita/matitaGui.ml +++ b/matita/matitaGui.ml @@ -363,7 +363,6 @@ class gui () = let main = new mainWin () in let fileSel = new fileSelectionWin () in let findRepl = new findReplWin () in - let newRoot = new newRootWin () in let keyBindingBoxes = (* event boxes which should receive global key events *) [ main#mainWinEventBox ] in @@ -387,7 +386,6 @@ class gui () = val mutable _ok_not_exists = false val mutable _only_directory = false val mutable font_size = default_font_size - val mutable next_root_must_contain = None val mutable next_ligatures = [] val clipboard = GData.clipboard Gdk.Atom.clipboard val primary = GData.clipboard Gdk.Atom.primary @@ -721,26 +719,6 @@ class gui () = f (); source_view#misc#grab_focus () with exc -> source_view#misc#grab_focus (); raise exc in - (* add root win *) - connect_button newRoot#addButton - (fun () -> - let name = newRoot#buriEntry#text in - let root = newRoot#rootEntry#text in - if next_root_must_contain = Some "xxx" then (); - HLog.error ("implement me: "^root^" "^name); - newRoot#buriEntry#set_text ""; - newRoot#rootEntry#set_text ""; - newRoot#toplevel#misc#hide()); - connect_button newRoot#chooseRootButton - (fun () -> - let path = self#chooseDir () in - match path with - | Some path -> newRoot#rootEntry#set_text path - | None -> ()); - connect_button newRoot#cancelButton - (fun () -> newRoot#toplevel#misc#hide ()); - ignore(newRoot#toplevel#event#connect#delete - (fun _ -> newRoot#toplevel#misc#hide();true)); (* file selection win *) ignore (fileSel#fileSelectionWin#event#connect#delete (fun _ -> true)); @@ -1188,7 +1166,6 @@ class gui () = method fileSel = fileSel method findRepl = findRepl method main = main - method newRoot = newRoot method newBrowserWin () = object (self) @@ -1242,10 +1219,6 @@ class gui () = (* we should check that this is a directory *) chosen_file - method createRoot ~containing = - next_root_must_contain <- containing; - newRoot#toplevel#misc#show() - method askText ?(title = "") ?(msg = "") () = let dialog = new textDialog () in dialog#textDialog#set_title title; diff --git a/matita/matitaGuiTypes.mli b/matita/matitaGuiTypes.mli index 5a166fbd4..c9ef86123 100644 --- a/matita/matitaGuiTypes.mli +++ b/matita/matitaGuiTypes.mli @@ -49,7 +49,6 @@ object method fileSel : MatitaGeneratedGui.fileSelectionWin method main : MatitaGeneratedGui.mainWin method findRepl : MatitaGeneratedGui.findReplWin - method newRoot: MatitaGeneratedGui.newRootWin (* method toolbar : MatitaGeneratedGui.toolBarWin *) method console: console @@ -86,7 +85,6 @@ 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 createRoot: containing:string option -> unit (** prompt the user for a (multiline) text entry *) method askText: ?title:string -> ?msg:string -> unit -> string option diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml index b0b020f01..1a7c86bb8 100644 --- a/matita/matitaScript.ml +++ b/matita/matitaScript.ml @@ -691,7 +691,6 @@ class script ~(source_view: GSourceView.source_view) ~set_star ~ask_confirmation ~urichooser - ~rootcreator () = let buffer = source_view#buffer in let source_buffer = source_view#source_buffer in @@ -733,7 +732,8 @@ object (self) method has_name = filename_ <> None method include_paths = - include_paths_ + include_paths_ @ + Helm_registry.get_list Helm_registry.string "matita.includes" method private curdir = try @@ -1146,10 +1146,10 @@ end let _script = ref None -let script ~source_view ~mathviewer ~urichooser ~rootcreator ~ask_confirmation ~set_star () +let script ~source_view ~mathviewer ~urichooser ~ask_confirmation ~set_star () = let s = new script - ~source_view ~mathviewer ~ask_confirmation ~urichooser ~rootcreator ~set_star () + ~source_view ~mathviewer ~ask_confirmation ~urichooser ~set_star () in _script := Some s; s diff --git a/matita/matitaScript.mli b/matita/matitaScript.mli index d4c82321e..6b6837999 100644 --- a/matita/matitaScript.mli +++ b/matita/matitaScript.mli @@ -93,7 +93,6 @@ val script: source_view:GSourceView.source_view -> mathviewer: MatitaTypes.mathViewer-> urichooser: (UriManager.uri list -> UriManager.uri list) -> - rootcreator: (containing:string option -> unit) -> ask_confirmation: (title:string -> message:string -> [`YES | `NO | `CANCEL]) -> set_star: (bool -> unit) -> -- 2.39.2