-matita.cmo: matitaTypes.cmo matitaScript.cmi matitaMisc.cmi \
- matitaMathView.cmi matitaLog.cmi matitaGui.cmi matitaGtkMisc.cmi \
- matitaEngine.cmi matitaDisambiguator.cmi buildTimeConf.cmo
-matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
- matitaMathView.cmx matitaLog.cmx matitaGui.cmx matitaGtkMisc.cmx \
- matitaEngine.cmx matitaDisambiguator.cmx buildTimeConf.cmx
+matitacleanLib.cmo: matitaSync.cmi matitaMisc.cmi matitaDb.cmi \
+ matitacleanLib.cmi
+matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaDb.cmx \
+ matitacleanLib.cmi
+matitaclean.cmo: matitacleanLib.cmi matitaDb.cmi
+matitaclean.cmx: matitacleanLib.cmx matitaDb.cmx
+matitacLib.cmo: matitaTypes.cmo matitaMisc.cmi matitaLog.cmi matitaExcPp.cmi \
+ matitaEngine.cmi buildTimeConf.cmo matitacLib.cmi
+matitacLib.cmx: matitaTypes.cmx matitaMisc.cmx matitaLog.cmx matitaExcPp.cmx \
+ matitaEngine.cmx buildTimeConf.cmx matitacLib.cmi
+matitac.cmo: matitacLib.cmi
+matitac.cmx: matitacLib.cmx
matitaDb.cmo: matitaMisc.cmi matitaDb.cmi
matitaDb.cmx: matitaMisc.cmx matitaDb.cmi
+matitadep.cmo: matitaMisc.cmi matitaExcPp.cmi
+matitadep.cmx: matitaMisc.cmx matitaExcPp.cmx
matitaDisambiguator.cmo: matitaTypes.cmo matitaDisambiguator.cmi
matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi
matitaEngine.cmo: matitaTypes.cmo matitaSync.cmi matitaMisc.cmi matitaLog.cmi \
matitaMathView.cmi
matitaMisc.cmo: matitaTypes.cmo buildTimeConf.cmo matitaMisc.cmi
matitaMisc.cmx: matitaTypes.cmx buildTimeConf.cmx matitaMisc.cmi
-matitaScript.cmo: matitaTypes.cmo matitaSync.cmi matitaMisc.cmi matitaLog.cmi \
- matitaEngine.cmi matitaDisambiguator.cmi matitaDb.cmi matitaScript.cmi
-matitaScript.cmx: matitaTypes.cmx matitaSync.cmx matitaMisc.cmx matitaLog.cmx \
- matitaEngine.cmx matitaDisambiguator.cmx matitaDb.cmx matitaScript.cmi
+matita.cmo: matitaTypes.cmo matitaScript.cmi matitaMisc.cmi \
+ matitaMathView.cmi matitaLog.cmi matitaGui.cmi matitaGtkMisc.cmi \
+ matitaEngine.cmi matitaDisambiguator.cmi buildTimeConf.cmo
+matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
+ matitaMathView.cmx matitaLog.cmx matitaGui.cmx matitaGtkMisc.cmx \
+ matitaEngine.cmx matitaDisambiguator.cmx buildTimeConf.cmx
+matitaScript.cmo: matitacleanLib.cmi matitaTypes.cmo matitaSync.cmi \
+ matitaMisc.cmi matitaLog.cmi matitaEngine.cmi matitaDisambiguator.cmi \
+ matitaDb.cmi matitaScript.cmi
+matitaScript.cmx: matitacleanLib.cmx matitaTypes.cmx matitaSync.cmx \
+ matitaMisc.cmx matitaLog.cmx matitaEngine.cmx matitaDisambiguator.cmx \
+ matitaDb.cmx matitaScript.cmi
matitaSync.cmo: matitaTypes.cmo matitaMisc.cmi matitaLog.cmi matitaDb.cmi \
matitaSync.cmi
matitaSync.cmx: matitaTypes.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \
matitaSync.cmi
matitaTypes.cmo: matitaLog.cmi
matitaTypes.cmx: matitaLog.cmx
-matitac.cmo: matitacLib.cmi
-matitac.cmx: matitacLib.cmx
-matitacLib.cmo: matitaTypes.cmo matitaMisc.cmi matitaLog.cmi matitaExcPp.cmi \
- matitaEngine.cmi buildTimeConf.cmo matitacLib.cmi
-matitacLib.cmx: matitaTypes.cmx matitaMisc.cmx matitaLog.cmx matitaExcPp.cmx \
- matitaEngine.cmx buildTimeConf.cmx matitacLib.cmi
-matitaclean.cmo: matitacleanLib.cmi matitaDb.cmi
-matitaclean.cmx: matitacleanLib.cmx matitaDb.cmx
-matitacleanLib.cmo: matitaSync.cmi matitaMisc.cmi matitaDb.cmi \
- matitacleanLib.cmi
-matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaDb.cmx \
- matitacleanLib.cmi
-matitadep.cmo: matitaMisc.cmi matitaExcPp.cmi
-matitadep.cmx: matitaMisc.cmx matitaExcPp.cmx
matitaDisambiguator.cmi: matitaTypes.cmo
matitaEngine.cmi: matitaTypes.cmo
matitaGtkMisc.cmi: matitaGeneratedGui.cmi
all: matita matitac matitatop cicbrowser matitadep matitaclean
-updater: $(LIB_DEPS)
- $(OCAMLC) $(PKGS) -linkpkg -o $@ updater.ml
-
ifeq ($(HAVE_OCAMLOPT),yes)
CMXS = $(patsubst %.cmo,%.cmx,$(CMOS))
CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS))
<key name="database">matita</key>
</section>
<section name="getter">
- <!-- <key name="prefetch">false</key> -->
- <key name="prefetch">@@PREFETCH@@</key>
- <key name="servers">
- file:///projects/helm/library/coq_contribs
- </key>
<key name="cache_dir">.matita/getter/cache</key>
- <key name="maps_dir">.matita/getter/maps</key>
<key name="dtd_dir">/projects/helm/xml/dtd</key>
+ <key name="prefix">
+ cic:/
+ file:///projects/helm/library/coq_contribs/
+ </key>
+ <key name="prefix">
+ cic:/matita/
+ .matita/xml/matita/
+ </key>
</section>
</helm_registry>
(MatitaMathView.sequentViewer_instance ())#get_selected_terms);
addDebugItem "dump getter settings" (fun _ ->
prerr_endline (Http_getter_env.env_to_string ()));
- addDebugItem "getter: update"
- (fun _ ->
- ignore (Thread.create (fun () ->
- MatitaLog.message "Rebuilding getter maps in background ...";
- Http_getter.update ();
- MatitaLog.message "Getter maps successfully rebuilt.") ()));
addDebugItem "getter: getalluris" (fun _ ->
List.iter prerr_endline (Http_getter.getalluris ()));
addDebugItem "dump script status" script#dump;
(** </DEBUGGING> *)
let _ =
- at_exit
- (fun () ->
- Http_getter_logger.log "Sync map tree to disk...";
- Http_getter.sync_dump_file ();
- print_endline "\nThanks for using Matita!\n");
+ at_exit (fun () -> print_endline "\nThanks for using Matita!\n");
Sys.catch_break true;
(try
gui#loadScript Sys.argv.(1);
let xpointer_RE = Pcre.regexp "#.*$"
+let file_scheme_RE = Pcre.regexp "^file://"
let clean_owner_environment () =
let dbd = instance () in
(fun uri ->
let uri = Pcre.replace ~rex:xpointer_RE ~templ:"" uri in
List.iter
- (fun suffix ->
- (*prerr_endline ("unregistering " ^ uri ^ suffix);*)
- Http_getter.unregister (uri ^ suffix))
-
+ (fun suffix -> Http_getter_storage.remove (uri ^ suffix ^ ".xml.gz"))
[""; ".body"; ".types"])
owned_uris;
List.iter (fun statement ->
match coercion with
| Cic.Const (uri,_)
| Cic.Var (uri,_) ->
- let o,_ =
- CicEnvironment.get_obj CicUniv.empty_ugraph uri
- in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
(match o with
| Cic.Constant (_,_,ty,_,_)
| Cic.Variable (_,_,ty,_,_) ->
uri,ty
| _ -> assert false)
| Cic.MutConstruct (uri,t,c,_) ->
- let o,_ =
- CicEnvironment.get_obj CicUniv.empty_ugraph uri
- in
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
(match o with
| Cic.InductiveDefinition (l,_,_,_) ->
let (_,_,_,cl) = List.nth l t in
* http://helm.cs.unibo.it/
*)
-open MatitaTypes;;
-open Printf;;
+open Printf
let to_string =
function
- | Option_error ("baseuri", "not found" ) ->
- "Baseuri not set for this script. Use 'set \"baseuri\" \"<uri>\".' to set it."
+ | MatitaTypes.Option_error ("baseuri", "not found" ) ->
+ "Baseuri not set for this script. "
+ ^ "Use 'set \"baseuri\" \"<uri>\".' to set it."
+ | MatitaTypes.Command_error msg -> "Error: " ^ msg
| CicTextualParser2.Parse_error (floc,err) ->
let (x, y) = CicAst.loc_of_floc floc in
sprintf "Parse error at %d-%d: %s" x y err
+ | UriManager.IllFormedUri uri -> sprintf "invalid uri: %s" uri
+ | CicEnvironment.Object_not_found uri ->
+ sprintf "object not found: %s" (UriManager.string_of_uri uri)
| exn -> "Uncaught exception: " ^ Printexc.to_string exn
+
| `String of string
]
-exception Browser_failure of string
-
class type cicBrowser =
object
method load: MatitaTypes.mathViewer_entry -> unit
method loadInput: string -> unit
end
+let reloadable = function
+ | `About `Current_proof
+ | `Dir _ ->
+ true
+ | _ -> false
+
class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
()
=
let whelp_RE = Pcre.regexp "^\\s*whelp" in
let uri_RE =
Pcre.regexp
- "^cic:/(\\w+/)*\\w+\\.(con|ind|var)(#xpointer\\(\\d+(/\\d+)+\\))?$"
+ "^cic:/([^/]+/)*[^/]+\\.(con|ind|var)(#xpointer\\(\\d+(/\\d+)+\\))?$"
in
- let dir_RE = Pcre.regexp "^cic:((/(\\w+/)*\\w+(/)?)|/|)$" in
+ let dir_RE = Pcre.regexp "^cic:((/([^/]+/)*[^/]+(/)?)|/|)$" in
let whelp_query_RE = Pcre.regexp "^\\s*whelp\\s+([^\\s]+)\\s+(.*)$" in
let trailing_slash_RE = Pcre.regexp "/$" in
let has_xpointer_RE = Pcre.regexp "#xpointer\\(\\d+/\\d+(/\\d+)?\\)$" in
let handle_error f =
try
f ()
- with exn ->
- fail (MatitaExcPp.to_string exn)
+ with exn -> fail (MatitaExcPp.to_string exn)
in
let handle_error' f = (fun () -> handle_error (fun () -> f ())) in
object (self)
GMain.quit ();
false));
ignore(win#whelpResultTreeview#connect#row_activated
- ~callback:(fun _ _ -> self#loadInput (self#_getSelectedUri ())));
+ ~callback:(fun _ _ ->
+ handle_error (fun () -> self#loadInput (self#_getSelectedUri ()))));
mathView#set_href_callback (Some (fun uri ->
- handle_error (fun () -> self#load (`Uri (UriManager.uri_of_string uri)))));
+ handle_error (fun () ->
+ self#load (`Uri (UriManager.uri_of_string uri)))));
self#_load (`About `Blank);
toplevel#show ()
val model =
new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview
+ val mutable lastDir = "" (* last loaded "directory" *)
+
method private _getSelectedUri () =
match model#easy_selection () with
| [sel] when is_uri sel -> sel (* absolute URI selected *)
- | [sel] -> win#browserUri#entry#text ^ sel (* relative URI selected *)
+(* | [sel] -> win#browserUri#entry#text ^ sel |+ relative URI selected +| *)
+ | [sel] -> lastDir ^ sel
| _ -> assert false
(** history RATIONALE
* @param uri string *)
method private _load entry =
try
- if entry <> current_entry || entry = `About `Current_proof then begin
- (match entry with
- | `About `Current_proof -> self#home ()
- | `About `Blank -> self#blank ()
- | `About `Us -> () (* TODO implement easter egg here :-] *)
- | `Check term -> self#_loadCheck term
- | `Cic (term, metasenv) -> self#_loadTermCic term metasenv
- | `Dir dir -> self#_loadDir dir
- | `Uri uri -> self#_loadUriManagerUri uri
- | `Whelp (query, results) ->
- set_whelp_query query;
- self#_loadList (List.map (fun r -> "obj", UriManager.string_of_uri r) results));
- self#setEntry entry
- end
- with
- | UriManager.IllFormedUri uri -> fail (sprintf "invalid uri: %s" uri)
- | CicEnvironment.Object_not_found uri ->
- fail (sprintf "object not found: %s" (UriManager.string_of_uri uri))
- | Browser_failure msg -> fail msg
+ if entry <> current_entry || reloadable entry then begin
+ (match entry with
+ | `About `Current_proof -> self#home ()
+ | `About `Blank -> self#blank ()
+ | `About `Us -> () (* TODO implement easter egg here :-] *)
+ | `Check term -> self#_loadCheck term
+ | `Cic (term, metasenv) -> self#_loadTermCic term metasenv
+ | `Dir dir -> self#_loadDir dir
+ | `Uri uri -> self#_loadUriManagerUri uri
+ | `Whelp (query, results) ->
+ set_whelp_query query;
+ self#_loadList (List.map (fun r -> "obj",
+ UriManager.string_of_uri r) results));
+ self#setEntry entry
+ end
+ with exn -> fail (MatitaExcPp.to_string exn)
method private blank () =
self#_showMath;
| Http_getter_types.Ls_object o -> "obj", o.Http_getter_types.uri)
content
in
- if l = [] then raise (Browser_failure "no such directory");
+ lastDir <- dir;
self#_loadList l
method private setEntry entry =
(try
entry_of_string txt
with Invalid_argument _ ->
- raise (Browser_failure (sprintf "unsupported uri: %s" txt)))
+ command_error (sprintf "unsupported uri: %s" txt))
in
self#_load entry;
self#_historyAdd entry
method history = history
method currentEntry = current_entry
method refresh () =
- if current_entry = `About `Current_proof then
- self#_load (`About `Current_proof)
- end
+ if reloadable current_entry then self#_load current_entry
+ end
let sequentsViewer ~(notebook:GPack.notebook)
~(sequentViewer:sequentViewer) ()
method goto_sequent: int -> unit (* to be called _after_ load_sequents *)
end
-exception Browser_failure of string
-
class type cicBrowser =
object
method load: MatitaTypes.mathViewer_entry -> unit
(List.map Filename.dirname [innertypespath; xmlpath]);
(* now write to disk *)
ensure_path_exists innertypespath;
- Xml.pp ~gzip:true xmlinnertypes (Some innertypespath) ;
+ Xml.pp ~gzip:true xmlinnertypes (Some innertypespath);
ensure_path_exists xmlpath;
Xml.pp ~gzip:true xml (Some xmlpath) ;
- (* now register to the getter *)
- Http_getter.register' innertypesuri (path_scheme_of innertypespath);
- Http_getter.register' uri (path_scheme_of xmlpath);
(* we return a list of uri,path we registered/created *)
(uri,xmlpath) :: (innertypesuri,innertypespath) ::
(* now the optional body, both write and register *)
None,None -> []
| Some bodyxml,Some bodyuri->
ensure_path_exists xmlbodypath;
- Xml.pp ~gzip:true bodyxml (Some xmlbodypath) ;
- Http_getter.register' bodyuri (path_scheme_of xmlbodypath);
- [bodyuri,xmlbodypath]
+ Xml.pp ~gzip:true bodyxml (Some xmlbodypath);
+ [bodyuri, xmlbodypath]
| _-> assert false)
-let remove_object_from_disk uri path =
- Sys.remove path;
- Http_getter.unregister' uri
-
let add_obj uri obj status =
let dbd = MatitaDb.instance () in
let suri = UriManager.string_of_uri uri in
let remove_coercion uri =
CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri)
+let safe_remove fname = if Sys.file_exists fname then Sys.remove fname
+
let time_travel ~present ~past =
let list_of_objs_to_remove = List.rev (delta_status past present) in
(* List.rev is just for the debugging code, which otherwise may list both
* something.ind and something.ind#xpointer ... (ask Enrico :-) *)
let debug_list = ref [] in
List.iter (fun (uri,p) ->
- remove_object_from_disk uri p;
+ safe_remove p;
remove_coercion uri;
(try
CicEnvironment.remove_obj uri
MatitaLog.debug "l2:";
List.iter MatitaLog.debug l2
-
let remove uri =
let derived_uris_of_uri uri =
UriManager.innertypesuri_of_uri uri ::
- UriManager.annuri_of_uri uri ::
(match UriManager.bodyuri_of_uri uri with
| None -> []
| Some u -> [u])
List.iter
(fun uri ->
(try
- let path =
- let path = Http_getter.resolve' (UriManager.strip_xpointer uri) in
- assert (String.sub path 0 7 = "file://");
- String.sub path 7 (String.length path - 7)
- in
MatitaLog.debug ("Removing: " ^ UriManager.string_of_uri uri);
- remove_object_from_disk uri path;
- with
- Http_getter_types.Key_not_found _ -> Http_getter.unregister' uri);
+ safe_remove (Http_getter.resolve' uri)
+ with Http_getter_types.Key_not_found _ -> ());
remove_coercion uri;
- ignore(MatitaDb.remove_uri uri))
+ ignore (MatitaDb.remove_uri uri))
to_remove
-
-
+
val set_proof_aliases :
MatitaTypes.status -> DisambiguateTypes.environment -> MatitaTypes.status
-
(* removes the object from DB, Disk, CoercionsDB, getter
* asserts the uri is resolved to file:// so it is only for
* user's objects *)
MatitaDb.create_owner_environment ();
*)
status := Some (ref (Lazy.force MatitaEngine.initial_status));
- at_exit
- (fun () ->
- Http_getter_logger.log "Sync map tree to disk...";
- Http_getter.sync_dump_file ();
- print_endline "\nThanks for using Matita!\n");
Sys.catch_break true;
let fname = fname () in
try
| CicTextualParser2.Parse_error (floc,err) ->
let (x, y) = CicAst.loc_of_floc floc in
MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err);
- Http_getter.sync_dump_file ();
if mode = `COMPILER then
exit 1
else
pp_ocaml_mode ()
+
-module HGT = Http_getter_types;;
-module HG = Http_getter;;
module UM = UriManager;;
module TA = TacticAst;;
let _ =
Helm_registry.load_from "matita.conf.xml";
- HG.init ();
+ Http_getter.init ();
MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner")
let main uri_to_remove = MatitacleanLib.clean_baseuris uri_to_remove
exit 1
let _ =
- at_exit
- (fun () ->
- Http_getter_logger.log "Sync map tree to disk...";
- Http_getter.sync_dump_file ();
- print_endline "\nThanks for using Matita!\n");
if Array.length Sys.argv < 2 then usage ();
if Sys.argv.(1) = "all" then
begin
+++ /dev/null
-let main () =
- Helm_registry.load_from "matita.conf.xml";
- Http_getter.init ();
- MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
- Http_getter.update ();
- Http_getter.sync_dump_file ()
-;;
-
-main ()
-
(** {2 Parser internals} *)
+let has_gz_suffix fname =
+ try
+ let idx = String.rindex fname '.' in
+ let suffix = String.sub fname idx (String.length fname - idx) in
+ suffix = ".gz"
+ with Not_found -> false
+
let parse uri filename =
let ctxt = new_parser_context uri in
ctxt.filename <- filename;
ctxt.xml_parser <- Some xml_parser;
try
(try
- P.parse xml_parser (`Gzip_file filename);
+ let xml_source =
+ if has_gz_suffix filename then `Gzip_file filename
+ else `File filename
+ in
+ P.parse xml_parser xml_source
with exn ->
ctxt.xml_parser <- None;
(* ZACK: the above "<- None" is vital for garbage collection. Without it
when Str.string_match body_RE uri 0 ->
parse uri tmpfile1 None
| CicParser.Parser_failure msg ->
- printf "%s FAILED (%s)\n" uri msg; flush stdout);
- unlink tmpfile1;
- (match tmpfile2 with None -> () | Some f -> unlink f)
+ printf "%s FAILED (%s)\n" uri msg; flush stdout)
let _ =
try
match UriManager.bodyuri_of_uri uri with
None -> None
| Some bodyuri ->
- try
- ignore (Http_getter.resolve' bodyuri) ;
- (* The body exists ==> it is not an axiom *)
- Some (Http_getter.getxml' bodyuri)
- with
- Http_getter_types.Key_not_found _ ->
- (* The body does not exist ==> we consider it an axiom *)
+ if Http_getter.exists' bodyuri then
+ Some (Http_getter.getxml' bodyuri)
+ else
None
in
- let cleanup () =
- Unix.unlink filename ;
- (*
- begin
- match filename_univ with
- Some f -> Unix.unlink f
- | None -> ()
- end;
- *)
- begin
- match bodyfilename with
- Some f -> Unix.unlink f
- | None -> ()
- end
- in
(* restarts the numbering of named universes (the ones inside the cic) *)
let _ = CicUniv.restart_numbering () in
let obj =
!total_parsing_time +. ((Unix.gettimeofday()) -. time );
rc
with exn ->
- cleanup ();
(match exn with
| CicParser.Getter_failure ("key_not_found", uri) ->
raise (Object_not_found (UriManager.uri_of_string uri))
| _ -> raise exn)
in
- let ugraph,filename_univ =
+ let ugraph,filename_univ =
(* FIXME: decomment this when the universes will be part of the library
try
let filename_univ =
***********************************************)
(Some CicUniv.empty_ugraph,None)
in
- cleanup();
- obj,ugraph
- with
- Http_getter_types.Key_not_found _ -> raise (Object_not_found uri)
+ obj,ugraph
+ with Http_getter_types.Key_not_found _ -> raise (Object_not_found uri)
;;
(* this is the function to fetch the object in the unchecked list and
let add_type_checked_obj uri (obj,ugraph) =
Cache.add_cooked ~key:uri (obj,ugraph)
-let in_library uri =
- in_cache uri ||
- (try
- ignore (Http_getter.resolve' uri);
- true
- with Http_getter_types.Key_not_found _ -> false)
+let in_library uri = in_cache uri || Http_getter.exists' uri
let remove_obj = Cache.remove
Helm_registry.load_from "extractor.conf.xml";
Http_getter.init ();
print_endline "Updating the getter....";
- Http_getter.update ();
let base = (Helm_registry.get "tmp.dir") ^ "/maps" in
let formats i =
(Helm_registry.get "tmp.dir") ^ "/"^(string_of_int i)^"/maps"
projects / helm.git / commitdiff