From fa0347cc0a604ba8743da9479117e1f13ab60482 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 5 Jan 2008 14:31:40 +0000 Subject: [PATCH] modifications to make matita behave reasonably, removed some useless windows --- components/extlib/hExtlib.ml | 18 ++- components/extlib/hExtlib.mli | 6 +- components/grafite_engine/grafiteEngine.ml | 4 +- components/grafite_engine/grafiteSync.ml | 2 +- components/grafite_engine/grafiteTypes.ml | 16 +- components/grafite_engine/grafiteTypes.mli | 6 +- components/library/librarian.ml | 35 +---- components/library/librarian.mli | 7 +- matita/buildTimeConf.ml.in | 3 - matita/matita.ma.templ | 2 - matita/matita.ml | 9 +- matita/matitaGui.ml | 171 ++++++++------------- matita/matitaGuiTypes.mli | 2 +- matita/matitaInit.ml | 2 +- matita/matitaScript.ml | 57 +++++-- matita/matitaScript.mli | 14 +- matita/matitaWiki.ml | 13 +- matita/matitac.ml | 12 +- matita/matitacLib.ml | 1 - matita/template_makefile.in | 36 ----- matita/template_makefile_devel.in | 39 ----- 21 files changed, 169 insertions(+), 286 deletions(-) delete mode 100644 matita/template_makefile.in delete mode 100644 matita/template_makefile_devel.in diff --git a/components/extlib/hExtlib.ml b/components/extlib/hExtlib.ml index 2fba7f651..c32ed0bed 100644 --- a/components/extlib/hExtlib.ml +++ b/components/extlib/hExtlib.ml @@ -438,7 +438,7 @@ let normalize_path s = let find_in paths path = let rec aux = function - | [] -> raise (Failure "not found") + | [] -> raise (Failure "find_in") | p :: tl -> let path = normalize_path (p ^ "/" ^ path) in try @@ -450,7 +450,19 @@ let find_in paths path = aux paths with Unix.Unix_error _ | Failure _ -> raise - (Failure ("File " ^ path ^ " not found (or not readable) in: " ^ - String.concat ":" paths)) + (Failure "find_in") ;; +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 && (len1 = len2 || d2.[len1] = '/') +;; + +let touch s = + try close_out(open_out s) with Sys_error _ -> () +;; diff --git a/components/extlib/hExtlib.mli b/components/extlib/hExtlib.mli index 07de4bea6..0d8d0aeff 100644 --- a/components/extlib/hExtlib.mli +++ b/components/extlib/hExtlib.mli @@ -49,7 +49,8 @@ val normalize_path: string -> string (** /foo/./bar/..//baz -> /foo/baz *) val find: ?test:(string -> bool) -> string -> string list (** find_in paths name returns the first path^"/"^name such that - * is a regular file and the current user can 'stat' it. May raise Failure. *) + * is a regular file and the current user can 'stat' it. + * May raise (Failure "find_in") *) val find_in: string list -> string -> string (** {2 File I/O} *) @@ -119,3 +120,6 @@ val raise_localized_exception: offset:int -> Stdpp.location -> exn -> 'a (* size in KB (SLOW) *) val estimate_size: 'a -> int +(* is_prefix_of [prefix] [string] *) +val is_prefix_of: string -> string -> bool +val touch: string -> unit diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index 766408c13..dfe0c019f 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -711,8 +711,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status | GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) -> Setoids.add_relation id a aeq refl sym trans; status, [] (*CSC: TO BE FIXED *) - | GrafiteAst.Set (loc, name, value) -> - GrafiteTypes.set_option status name value,[] + | GrafiteAst.Set (loc, name, value) -> status, [] +(* GrafiteTypes.set_option status name value,[] *) | GrafiteAst.Obj (loc,obj) -> let ext,name = match obj with diff --git a/components/grafite_engine/grafiteSync.ml b/components/grafite_engine/grafiteSync.ml index ca3d873c5..b02481111 100644 --- a/components/grafite_engine/grafiteSync.ml +++ b/components/grafite_engine/grafiteSync.ml @@ -139,7 +139,7 @@ let init baseuri = { GrafiteTypes.moo_content_rev = []; proof_status = GrafiteTypes.No_proof; - options = GrafiteTypes.no_options; +(* options = GrafiteTypes.no_options; *) objects = []; coercions = []; universe = Universe.empty; diff --git a/components/grafite_engine/grafiteTypes.ml b/components/grafite_engine/grafiteTypes.ml index af819555b..71fd19f94 100644 --- a/components/grafite_engine/grafiteTypes.ml +++ b/components/grafite_engine/grafiteTypes.ml @@ -44,17 +44,19 @@ type proof_status = (* Status in which the proof could be while it is being processed by the * engine. No status entering/exiting the engine could be in it. *) +(* REMOVE module StringMap = Map.Make (String) type option_value = | String of string | Int of int -type options = option_value StringMap.t -let no_options = StringMap.empty +*) +(* type options = option_value StringMap.t *) +(* let no_options = StringMap.empty *) type status = { moo_content_rev: GrafiteMarshal.moo; proof_status: proof_status; - options: options; +(* options: options; *) objects: UriManager.uri list; coercions: UriManager.uri list; universe:Universe.universe; @@ -137,13 +139,14 @@ let add_moo_content cmds status = GrafiteAstPp.pp_command content')); *) { status with moo_content_rev = content' } +let get_baseuri status = status.baseuri;; + +(* let get_option status name = try StringMap.find name status.options with Not_found -> raise (Option_error (name, "not found")) -let get_baseuri status = status.baseuri;; - let set_option status name value = let types = [ (* no set options defined! *) ] in let ty_and_mangler = @@ -167,6 +170,7 @@ let get_string_option status name = match get_option status name with | String s -> s | _ -> raise (Option_error (name, "not a string value")) +*) let dump_status status = HLog.message "status.aliases:\n"; @@ -178,6 +182,7 @@ let dump_status status = | Proof _ -> "proof\n" | Intermediate _ -> "Intermediate\n"); HLog.message "status.options\n"; +(* REMOVEME StringMap.iter (fun k v -> let v = match v with @@ -185,6 +190,7 @@ let dump_status status = | Int i -> string_of_int i in HLog.message (k ^ "::=" ^ v)) status.options; +*) HLog.message "status.coercions\n"; HLog.message "status.objects:\n"; List.iter diff --git a/components/grafite_engine/grafiteTypes.mli b/components/grafite_engine/grafiteTypes.mli index 8d9b81ed8..ce988944b 100644 --- a/components/grafite_engine/grafiteTypes.mli +++ b/components/grafite_engine/grafiteTypes.mli @@ -42,16 +42,18 @@ type proof_status = | Proof of ProofEngineTypes.proof | Intermediate of Cic.metasenv +(* type option_value = | String of string | Int of int type options val no_options: options +*) type status = { moo_content_rev: GrafiteMarshal.moo; proof_status: proof_status; (** logical status *) - options: options; +(* options: options; *) objects: UriManager.uri list; (** in-scope objects *) coercions: UriManager.uri list; (** defined coercions *) universe:Universe.universe; (** universe of terms used by auto *) @@ -63,9 +65,11 @@ val dump_status : status -> unit (** list is not reversed, head command will be the first emitted *) val add_moo_content: GrafiteMarshal.ast_command list -> status -> status +(* REOMVE ME val get_option : status -> string -> option_value val get_string_option : status -> string -> string val set_option : status -> string -> string -> status +*) val get_baseuri: status -> string val get_current_proof: status -> ProofEngineTypes.proof diff --git a/components/library/librarian.ml b/components/library/librarian.ml index 4c25bc309..e8d0e7da1 100644 --- a/components/library/librarian.ml +++ b/components/library/librarian.ml @@ -1,4 +1,4 @@ -exception UnableToQualify +exception NoRootFor of string let find_root path = let paths = List.rev (Str.split (Str.regexp "/") path) in @@ -7,19 +7,10 @@ let find_root path = | [] -> ["/"] in let paths = List.map HExtlib.normalize_path (build paths) in - HExtlib.find_in paths "root" + try HExtlib.find_in paths "root" + with Failure "find_in" -> raise (NoRootFor 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 && (len1 = len2 || d2.[len1] = '/') -;; - let ensure_trailing_slash s = if s = "" then "/" else if s.[String.length s-1] <> '/' then s^"/" else s @@ -39,7 +30,8 @@ let find_root_for ~include_paths file = try let mburi = Helm_registry.get "matita.baseuri" in match Str.split (Str.regexp " ") mburi with - | [root; buri] when is_prefix_of root path -> ":registry:", root, buri + | [root; buri] when HExtlib.is_prefix_of root path -> + ":registry:", root, buri | _ -> raise (Helm_registry.Key_not_found "matita.baseuri") with Helm_registry.Key_not_found "matita.baseuri" -> let rootpath = find_root path in @@ -63,21 +55,6 @@ let find_root_for ~include_paths file = HLog.error (rootpath ^ " sets an incorrect baseuri: " ^ buri); ensure_trailing_slash root, remove_trailing_slash uri, path ;; - -let filename () = - try - Helm_registry.get "matita.filename" - with Helm_registry.Key_not_found "matita.filename" -> - try - match Helm_registry.get_list Helm_registry.string "matita.args" with - | [x] -> - HLog.warn ("Using matita.args as filename: "^x); - Helm_registry.set "matita.filename" x; - x - | _ -> raise (Failure "no (or more than one) filename to compile") - with Helm_registry.Key_not_found "matita.filename" -> - raise (Failure "Unable to get current file name") -;; let baseuri_of_script ?(include_paths=[]) file = let root, buri, path = find_root_for ~include_paths file in @@ -89,7 +66,7 @@ let baseuri_of_script ?(include_paths=[]) file = match l1, l2 with | h1::tl1,h2::tl2 when h1 = h2 -> substract tl1 tl2 | l,[] -> l - | _ -> raise UnableToQualify + | _ -> raise (NoRootFor file) in let extra_buri = substract lpath lroot in let chop name = diff --git a/components/library/librarian.mli b/components/library/librarian.mli index a8e10bf5a..a6b3c6849 100644 --- a/components/library/librarian.mli +++ b/components/library/librarian.mli @@ -1,9 +1,8 @@ -exception UnableToQualify +exception NoRootFor of string + val find_root : string -> string -val is_prefix_of : string -> string -> bool -val filename : unit -> string -(* baseuri_of_script ?(inc:REG[matita.includes] fname -> root, buri, fullpath +(* baseuri_of_script ?(inc:REG[matita.includes]) fname -> root, buri, fullpath * sample: baseuri_of_script a.ma -> /home/pippo/devel/, cic:/matita/a, * /home/pippo/devel/a.ma *) val baseuri_of_script: diff --git a/matita/buildTimeConf.ml.in b/matita/buildTimeConf.ml.in index ec01152c4..6f693a138 100644 --- a/matita/buildTimeConf.ml.in +++ b/matita/buildTimeConf.ml.in @@ -50,9 +50,6 @@ let core_notation_script = runtime_base_dir ^ "/core_notation.moo" let matita_conf = runtime_base_dir ^ "/matita.conf.xml" let closed_xml = runtime_base_dir ^ "/closed.xml" let gtkmathview_conf = runtime_base_dir ^ "/gtkmathview.matita.conf.xml" -let matitamake_makefile_template = runtime_base_dir ^ "/template_makefile.in" -let matitamake_makefile_template_devel = - runtime_base_dir ^ "/template_makefile_devel.in" let stdlib_dir_devel = runtime_base_dir ^ "/library" let stdlib_dir_installed = runtime_base_dir ^ "/ma/standard-library" let help_dir = runtime_base_dir ^ "/help" diff --git a/matita/matita.ma.templ b/matita/matita.ma.templ index ec1bc8006..5ec5164b8 100644 --- a/matita/matita.ma.templ +++ b/matita/matita.ma.templ @@ -12,5 +12,3 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/test/". - diff --git a/matita/matita.ml b/matita/matita.ml index 60b112d98..b3c0373eb 100644 --- a/matita/matita.ml +++ b/matita/matita.ml @@ -308,12 +308,9 @@ let _ = (fun _ -> prerr_endline "Still cleaning the library: don't be impatient!")); prerr_endline "Matita is cleaning up. Please wait."; - try - let baseuri = - GrafiteTypes.get_string_option - (MatitaScript.current ())#grafite_status "baseuri" - in + let baseuri = + GrafiteTypes.get_baseuri (MatitaScript.current ())#grafite_status + in LibraryClean.clean_baseuris [baseuri] - with GrafiteTypes.Option_error _ -> () (* vim:set foldmethod=marker: *) diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml index 1b1c136b9..ff1281fde 100644 --- a/matita/matitaGui.ml +++ b/matita/matitaGui.ml @@ -66,58 +66,30 @@ class console ~(buffer: GText.buffer) () = end let clean_current_baseuri grafite_status = - try - let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in - LibraryClean.clean_baseuris [baseuri] - with GrafiteTypes.Option_error _ -> () + LibraryClean.clean_baseuris [GrafiteTypes.get_baseuri grafite_status] -let ask_and_save_moo_if_needed parent fname lexicon_status grafite_status = - let baseuri = - try Some (GrafiteTypes.get_string_option grafite_status "baseuri") - with GrafiteTypes.Option_error _ -> None +let save_moo lexicon_status grafite_status = + let script = MatitaScript.current () in + let baseuri = GrafiteTypes.get_baseuri grafite_status in + let no_pstatus = + grafite_status.GrafiteTypes.proof_status = GrafiteTypes.No_proof in - if (MatitaScript.current ())#eos && - grafite_status.GrafiteTypes.proof_status = GrafiteTypes.No_proof && - baseuri <> None - then - begin - let baseuri = match baseuri with Some b -> b | None -> assert false in - let moo_fname = - LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri - ~writable:true in - let save () = - let lexicon_fname = + match script#bos, script#eos, no_pstatus with + | true, _, _ -> () + | _, true, true -> + let moo_fname = + LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri + ~writable:true in + let lexicon_fname = LibraryMisc.lexicon_file_of_baseuri ~must_exist:false ~baseuri ~writable:true - in - GrafiteMarshal.save_moo moo_fname - grafite_status.GrafiteTypes.moo_content_rev; - LexiconMarshal.save_lexicon lexicon_fname - lexicon_status.LexiconEngine.lexicon_content_rev - in - begin - let rc = - MatitaGtkMisc.ask_confirmation - ~title:"A .moo can be generated" - ~message:(Printf.sprintf - "%s can be generated for %s.\nShould I generate it?" - (Filename.basename moo_fname) (Filename.basename fname)) - ~parent () - in - let b = - match rc with - | `YES -> true - | `NO -> false - | `CANCEL -> raise MatitaTypes.Cancel - in - if b then - save () - else - clean_current_baseuri grafite_status - end - end - else - clean_current_baseuri grafite_status + in + GrafiteMarshal.save_moo moo_fname + grafite_status.GrafiteTypes.moo_content_rev; + LexiconMarshal.save_lexicon lexicon_fname + lexicon_status.LexiconEngine.lexicon_content_rev + | _ -> clean_current_baseuri grafite_status +;; let ask_unsaved parent = MatitaGtkMisc.ask_confirmation @@ -229,7 +201,8 @@ class interpErrorModel = end -let rec interactive_error_interp ~all_passes (source_buffer:GSourceView.source_buffer) notify_exn offset errorll script_fname +let rec interactive_error_interp ~all_passes + (source_buffer:GSourceView.source_buffer) notify_exn offset errorll filename = (* hook to save a script for each disambiguation error *) if false then @@ -237,7 +210,6 @@ let rec interactive_error_interp ~all_passes (source_buffer:GSourceView.source_b source_buffer#get_text ~start:source_buffer#start_iter ~stop:source_buffer#end_iter () in let md5 = Digest.to_hex (Digest.string text) in - let filename = match script_fname with Some s -> s | None -> "unnamed.ma" in let filename = Filename.chop_extension filename ^ ".error." ^ md5 ^ ".ma" in let ch = open_out filename in @@ -369,7 +341,7 @@ let rec interactive_error_interp ~all_passes (source_buffer:GSourceView.source_b connect_button dialog#disambiguationErrorsMoreErrors (fun _ -> return () ; interactive_error_interp ~all_passes:true source_buffer - notify_exn offset errorll script_fname); + notify_exn offset errorll filename); connect_button dialog#disambiguationErrorsCancelButton fail; dialog#disambiguationErrors#show (); GtkThread.main () @@ -414,7 +386,6 @@ class gui () = 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 val mutable next_ligatures = [] @@ -422,6 +393,7 @@ class gui () = val primary = GData.clipboard Gdk.Atom.primary initializer + let s () = MatitaScript.current () in (* glade's check widgets *) List.iter (fun w -> w#check_widgets ()) (let c w = (w :> unit>) in @@ -713,8 +685,9 @@ class gui () = with | GrafiteDisambiguator.DisambiguationError (offset,errorll) -> (try - interactive_error_interp ~all_passes:!all_disambiguation_passes source_buffer - notify_exn offset errorll script_fname + interactive_error_interp + ~all_passes:!all_disambiguation_passes source_buffer + notify_exn offset errorll (s())#filename with exc -> notify_exn exc); unlock_world () @@ -952,28 +925,27 @@ class gui () = source_buffer#set_language matita_lang; source_buffer#set_highlight true in - let s () = MatitaScript.current () in let disableSave () = - script_fname <- None; + (s())#assignFileName None; main#saveMenuItem#misc#set_sensitive false in let saveAsScript () = let script = s () in match self#chooseFile ~ok_not_exists:true () with | Some f -> - script#assignFileName f; + HExtlib.touch f; + script#assignFileName (Some f); script#saveToFile (); console#message ("'"^f^"' saved.\n"); self#_enableSaveTo f | None -> () in let saveScript () = - match script_fname with - | None -> saveAsScript () - | Some f -> - (s ())#assignFileName f; - (s ())#saveToFile (); - console#message ("'"^f^"' saved.\n"); + let script = s () in + if script#has_name then + (script#saveToFile (); + console#message ("'"^script#filename^"' saved.\n")) + else saveAsScript () in let abandon_script () = let lexicon_status = (s ())#lexicon_status in @@ -983,11 +955,7 @@ class gui () = | `YES -> saveScript () | `NO -> () | `CANCEL -> raise MatitaTypes.Cancel); - (match script_fname with - | None -> () - | Some fname -> - ask_and_save_moo_if_needed main#toplevel fname - lexicon_status grafite_status); + save_moo lexicon_status grafite_status in let loadScript () = let script = s () in @@ -996,7 +964,7 @@ class gui () = | Some f -> abandon_script (); script#reset (); - script#assignFileName f; + script#assignFileName (Some f); source_view#source_buffer#begin_not_undoable_action (); script#loadFromFile f; source_view#source_buffer#end_not_undoable_action (); @@ -1012,7 +980,7 @@ class gui () = (s ())#template (); source_view#source_buffer#end_not_undoable_action (); disableSave (); - script_fname <- None + (s ())#assignFileName None in let cursor () = source_buffer#place_cursor @@ -1029,38 +997,18 @@ class gui () = let jump = locker (keep_focus jump) in (* quit *) self#setQuitCallback (fun () -> - let lexicon_status = (MatitaScript.current ())#lexicon_status in - let grafite_status = (MatitaScript.current ())#grafite_status in + let script = MatitaScript.current () in if source_view#buffer#modified then - begin - let rc = ask_unsaved main#toplevel in - try - match rc with - | `YES -> saveScript (); - if not source_view#buffer#modified then - begin - (match script_fname with - | None -> () - | Some fname -> - ask_and_save_moo_if_needed main#toplevel - fname lexicon_status grafite_status); - GMain.Main.quit () - end - | `NO -> GMain.Main.quit () - | `CANCEL -> raise MatitaTypes.Cancel - with MatitaTypes.Cancel -> () - end + match ask_unsaved main#toplevel with + | `YES -> + saveScript (); + save_moo script#lexicon_status script#grafite_status; + GMain.Main.quit () + | `NO -> GMain.Main.quit () + | `CANCEL -> () else - begin - (match script_fname with - | None -> clean_current_baseuri grafite_status; GMain.Main.quit () - | Some fname -> - try - ask_and_save_moo_if_needed main#toplevel fname lexicon_status - grafite_status; - GMain.Main.quit () - with MatitaTypes.Cancel -> ()) - end); + (save_moo script#lexicon_status script#grafite_status; + GMain.Main.quit ())); connect_button main#scriptAdvanceButton advance; connect_button main#scriptRetractButton retract; connect_button main#scriptTopButton top; @@ -1248,12 +1196,12 @@ class gui () = ask_text ~gui:self ~title:"External editor" ~msg ~multiline:false ~default:(Helm_registry.get "matita.external_editor") () in *) - let fname = Librarian.filename () in + let script = MatitaScript.current () in + let fname = script#filename in let slice mark = source_buffer#start_iter#get_slice ~stop:(source_buffer#get_iter_at_mark mark) in - let script = MatitaScript.current () in let locked = `MARK script#locked_mark in let string_pos mark = string_of_int (String.length (slice mark)) in let cursor_pos = string_pos `INSERT in @@ -1302,7 +1250,7 @@ class gui () = in let data = Matitaprover.p_to_ma ~filename:file ~tptppath () in let filename = Pcre.replace ~pat:"\\.p$" ~templ:".ma" file in - script#assignFileName filename; + script#assignFileName (Some filename); source_view#source_buffer#begin_not_undoable_action (); script#loadFromString data; source_view#source_buffer#end_not_undoable_action (); @@ -1311,7 +1259,7 @@ class gui () = end else begin - script#assignFileName file; + script#assignFileName (Some file); let content = if Sys.file_exists file then file else BuildTimeConf.script_template @@ -1323,17 +1271,18 @@ class gui () = self#_enableSaveTo file end - method setStar name b = + method setStar b = + let s = MatitaScript.current () in let w = main#toplevel in let set x = w#set_title x in - let name = "Matita - " ^ name in - if b then - set (name ^ " *") - else - set (name) + let name = + "Matita - " ^ Filename.basename s#filename ^ + (if b then "*" else "") ^ + " in " ^ s#buri_of_current_file + in + set name method private _enableSaveTo file = - script_fname <- Some file; self#main#saveMenuItem#misc#set_sensitive true method console = console diff --git a/matita/matitaGuiTypes.mli b/matita/matitaGuiTypes.mli index 67d431040..71cda4ac9 100644 --- a/matita/matitaGuiTypes.mli +++ b/matita/matitaGuiTypes.mli @@ -93,7 +93,7 @@ object method askText: ?title:string -> ?msg:string -> unit -> string option method loadScript: string -> unit - method setStar: string -> bool -> unit + method setStar: bool -> unit (** {3 Fonts} *) method increaseFontSize: unit -> unit diff --git a/matita/matitaInit.ml b/matita/matitaInit.ml index 350d332ff..58aadf76f 100644 --- a/matita/matitaInit.ml +++ b/matita/matitaInit.ml @@ -45,7 +45,7 @@ let conffile = ref BuildTimeConf.matita_conf let registry_defaults = [ "matita.debug", "false"; "matita.external_editor", "gvim -f -c 'go %p' %f"; - "matita.preserve", "false"; + "matita.preserve", "false"; (* FIXME, inutile pure lei *) "matita.profile", "true"; "matita.system", "false"; "matita.verbose", "false"; diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml index c5239ffb4..c4cb286b3 100644 --- a/matita/matitaScript.ml +++ b/matita/matitaScript.ml @@ -753,27 +753,43 @@ let initial_statuses baseuri = let grafite_status = GrafiteSync.init baseuri in grafite_status,lexicon_status in +let default_buri = "cic:/matita/tests" in +let default_fname = ".unnamed.ma" in object (self) val mutable include_paths = Helm_registry.get_list Helm_registry.string "matita.includes" val scriptId = fresh_script_id () - + val guistuff = { mathviewer = mathviewer; urichooser = urichooser; ask_confirmation = ask_confirmation; - develcreator=develcreator;} + develcreator=develcreator; + } + + val mutable filename_ = (None : string option) + + method has_name = filename_ <> None + + method buri_of_current_file = + match filename_ with + | None -> default_buri + | Some f -> + try let root, buri, fname = Librarian.baseuri_of_script f in buri + with Librarian.NoRootFor _ -> default_buri + + method filename = match filename_ with None -> default_fname | Some f -> f initializer ignore (GMain.Timeout.add ~ms:300000 ~callback:(fun _ -> self#_saveToBackupFile ();true)); ignore (buffer#connect#modified_changed - (fun _ -> set_star (Filename.basename (Librarian.filename ())) buffer#modified)) + (fun _ -> set_star buffer#modified)) val mutable statements = [] (** executed statements *) - val mutable history = [ initial_statuses "cic:/matita/test/" ] + val mutable history = [ initial_statuses default_buri ] (** list of states before having executed statements. Head element of this * list is the current state, last element is the state at the beginning of * the script. @@ -932,21 +948,26 @@ object (self) buffer#set_modified false method assignFileName file = - let root, buri, file = Librarian.baseuri_of_script ~include_paths file in - Helm_registry.set "matita.filename" file; + self#goto_top; + filename_ <- file; self#reset_buffer method saveToFile () = - let oc = open_out (Librarian.filename ()) in - output_string oc (buffer#get_text ~start:buffer#start_iter + if self#has_name && buffer#modified then + let oc = open_out self#filename in + output_string oc (buffer#get_text ~start:buffer#start_iter ~stop:buffer#end_iter ()); - close_out oc; - buffer#set_modified false + close_out oc; + set_star false; + buffer#set_modified false + else + if self#has_name then HLog.debug "No need to save" + else HLog.error "Can't save, no filename selected" method private _saveToBackupFile () = if buffer#modified then begin - let f = Librarian.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 ()); @@ -968,10 +989,8 @@ object (self) LexiconSync.time_travel ~present:self#lexicon_status ~past:lexicon_status method private reset_buffer = - let file = Librarian.filename () in - let root, buri, file = Librarian.baseuri_of_script file in statements <- []; - history <- [ initial_statuses buri ]; + history <- [ initial_statuses self#buri_of_current_file ]; userGoal <- None; self#notify; buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter; @@ -988,7 +1007,7 @@ object (self) let template = HExtlib.input_file BuildTimeConf.script_template in buffer#insert ~iter:(buffer#get_iter `START) template; buffer#set_modified false; - set_star (Filename.basename (Librarian.filename ())) false + set_star false method goto (pos: [`Top | `Bottom | `Cursor]) () = try @@ -1098,6 +1117,11 @@ object (self) method setGoal n = userGoal <- n method goal = userGoal + method bos = + match history with + | _::[] -> true + | _ -> false + method eos = let rec is_there_only_comments lexicon_status s = if Pcre.pmatch ~rex:only_dust_RE s then raise Margin; @@ -1132,7 +1156,8 @@ prerr_endline ("## " ^ string_of_int parsed_text_length); HLog.debug ("history size: " ^ string_of_int (List.length history)); HLog.debug (sprintf "%d statements:" (List.length statements)); List.iter HLog.debug statements; - HLog.debug ("Current file name: " ^ Librarian.filename ()); + HLog.debug ("Current file name: " ^ self#filename); + HLog.debug ("Current buri: " ^ self#buri_of_current_file); end let _script = ref None diff --git a/matita/matitaScript.mli b/matita/matitaScript.mli index 2dd58b595..8f120b296 100644 --- a/matita/matitaScript.mli +++ b/matita/matitaScript.mli @@ -33,7 +33,7 @@ object method locked_tag : GText.tag method error_tag : GText.tag - (** @return current status *) + (** @return current status *) method lexicon_status: LexiconEngine.status method grafite_status: GrafiteTypes.status @@ -51,8 +51,12 @@ object method template: unit -> unit (** {2 Load/save} *) - - method assignFileName : string -> unit (* to the current active file *) + + method has_name: bool + (* alwais return a name, use has_name to check if it is the default one *) + method filename: string + method buri_of_current_file: string + method assignFileName : string option -> unit (* to the current active file *) method loadFromFile : string -> unit method loadFromString : string -> unit method saveToFile : unit -> unit @@ -62,7 +66,6 @@ object (** @return true if there is an ongoing proof, false otherise *) method onGoingProof: unit -> bool -(* method proofStatus: ProofEngineTypes.status |+* @raise Statement_error +| *) method proofMetasenv: Cic.metasenv (** @raise Statement_error *) method proofContext: Cic.context (** @raise Statement_error *) method proofConclusion: Cic.term (** @raise Statement_error *) @@ -73,6 +76,7 @@ object (** end of script, true if the whole script has been executed *) method eos: bool + method bos: bool (** misc *) method clean_dirty_lock: unit @@ -91,7 +95,7 @@ val script: develcreator: (containing:string option -> unit) -> ask_confirmation: (title:string -> message:string -> [`YES | `NO | `CANCEL]) -> - set_star: (string -> bool -> unit) -> + set_star: (bool -> unit) -> unit -> script diff --git a/matita/matitaWiki.ml b/matita/matitaWiki.ml index b5dc5ccf7..08f683cbf 100644 --- a/matita/matitaWiki.ml +++ b/matita/matitaWiki.ml @@ -66,13 +66,9 @@ let clean_exit n = match !grafite_status with [] -> exit n | grafite_status::_ -> - try - let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in + let baseuri = GrafiteTypes.get_baseuri grafite_status in LibraryClean.clean_baseuris ~verbose:false [baseuri]; exit n - with GrafiteTypes.Option_error("baseuri", "not found") -> - (* no baseuri ==> nothing to clean yet *) - exit n let terminate n = let terminator = String.make 1 (Char.chr 249) in @@ -248,10 +244,11 @@ let main () = else begin let baseuri = - GrafiteTypes.get_string_option - (match !grafite_status with + GrafiteTypes.get_baseuri + (match !grafite_status with [] -> assert false - | s::_ -> s) "baseuri" in + | s::_ -> s) + in let moo_fname = LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri ~writable:true diff --git a/matita/matitac.ml b/matita/matitac.ml index 868326a8d..8645d2175 100644 --- a/matita/matitac.ml +++ b/matita/matitac.ml @@ -135,17 +135,7 @@ let main_compiler () = with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> None ;; - let build fname = - let oldfname = - Helm_registry.get_opt - Helm_registry.string "matita.filename" - in - let rc = MatitacLib.compile fname in - (match oldfname with - | Some n -> Helm_registry.set_string "matita.filename" n; - | _ -> Helm_registry.unset "matita.filename"); - rc - ;; + let build = MatitacLib.compile;; end in let module Make = Make.Make(F) in diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml index 80e81c2d7..ee7a2eae5 100644 --- a/matita/matitacLib.ml +++ b/matita/matitacLib.ml @@ -94,7 +94,6 @@ let cut prefix s = ;; let rec compile fname = - Helm_registry.set_string "matita.filename" fname; (* initialization, MOVE OUTSIDE *) let matita_debug = Helm_registry.get_bool "matita.debug" in let clean_baseuri = not (Helm_registry.get_bool "matita.preserve") in diff --git a/matita/template_makefile.in b/matita/template_makefile.in deleted file mode 100644 index ac3e14498..000000000 --- a/matita/template_makefile.in +++ /dev/null @@ -1,36 +0,0 @@ -SRC=$(shell find @ROOT@ -name "*.ma" -a -type f) -SHORTSRC=$(echo $(SRC) | sed 's?^@ROOT@/??g') -TODO=$(SRC:%.ma=%.mo) - -MATITA_FLAGS= -MATITA_FLAGS+=-noprofile -NODB=false -ifeq ($(NODB),true) - MATITA_FLAGS += -nodb -endif - -MATITAC=@CC@ -MATITACLEAN=@CLEAN@ -MATITADEP=@DEP@ - -all: $(TODO) - -clean: - $(MATITACLEAN) $(MATITA_FLAGS) $(SRC) - rm -f $(TODO) @DEPFILE@ - -%.moo: - if [ -z "$<" ]; then \ - echo "missing dependencies for $@"; \ - else \ - $(MATITAC) $(MATITA_FLAGS) -q -I @ROOT@ $<; \ - fi - -@DEPFILE@ : $(SRC) - $(MATITADEP) $(MATITA_FLAGS) -I '@ROOT@' -dot @DEPFILE@.dot $^ \ - 1> @DEPFILE@ 2>@DEPFILE@.errors \ - || (echo;cat @DEPFILE@.errors;echo;rm @DEPFILE@;false) - -# this is the depend for full targets like: -# dir/dir/name.moo: dir/dir/name.ma dir/dep.moo -include @DEPFILE@ diff --git a/matita/template_makefile_devel.in b/matita/template_makefile_devel.in deleted file mode 100644 index 98b7c1f20..000000000 --- a/matita/template_makefile_devel.in +++ /dev/null @@ -1,39 +0,0 @@ -H=@ - -RT_BASEDIR=$(shell if [ -x "@MATITA_RT_BASE_DIR@/matitamake" -o -x "@MATITA_RT_BASE_DIR@/matitamake.opt" ]; then echo "@MATITA_RT_BASE_DIR@"; else echo ""; fi) -OPTIONS=-bench -MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS) -CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) -MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS) -CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS) - -devel:=$(shell basename `pwd`) - -ifneq "$(SRC)" "" - XXX="SRC=$(SRC)" -endif - -all: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel) -clean: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel) -cleanall: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all - -all.opt opt: preall.opt - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel) -clean.opt: preall.opt - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel) -cleanall.opt: preall.opt - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all - -%.mo: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@ -%.mo.opt: preall.opt - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $(@:.opt=) - -preall: - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel) - -preall.opt: - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) init $(devel) -- 2.39.2