let debug_print = if debug then prerr_endline else ignore ;;
let eval_from_stream
- ?do_heavy_checks ?include_paths ?clean_baseuri status str cb
+ ?do_heavy_checks ~include_paths ?clean_baseuri status str cb
=
try
while true do
cb !status ast;
status :=
GrafiteEngine.eval_ast
+ ~baseuri_of_script:(GrafiteParserMisc.baseuri_of_script ~include_paths)
~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
~disambiguate_command:GrafiteDisambiguate.disambiguate_command
- ?do_heavy_checks ?include_paths ?clean_baseuri !status ast
+ ?do_heavy_checks ?clean_baseuri !status ast
done
with End_of_file -> ()
let eval_from_stream_greedy
- ?do_heavy_checks ?include_paths ?clean_baseuri status str cb
+ ?do_heavy_checks ~include_paths ?clean_baseuri status str cb
=
while true do
print_string "matita> ";
cb !status ast;
status :=
GrafiteEngine.eval_ast
+ ~baseuri_of_script:(GrafiteParserMisc.baseuri_of_script ~include_paths)
~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
~disambiguate_command:GrafiteDisambiguate.disambiguate_command
- ?do_heavy_checks ?include_paths ?clean_baseuri !status ast
+ ?do_heavy_checks ?clean_baseuri !status ast
done
;;
-let eval_string ?do_heavy_checks ?include_paths ?clean_baseuri status str =
+let eval_string ?do_heavy_checks ~include_paths ?clean_baseuri status str =
eval_from_stream
- ?do_heavy_checks ?include_paths ?clean_baseuri status
+ ?do_heavy_checks ~include_paths ?clean_baseuri status
(Ulexing.from_utf8_string str) (fun _ _ -> ())
let default_options () = no_options
* infos like if the theorem is a duplicate *)
val eval_string:
?do_heavy_checks:bool ->
- ?include_paths:string list ->
+ include_paths:string list ->
?clean_baseuri:bool ->
GrafiteTypes.status ref -> string -> unit
val eval_from_stream:
?do_heavy_checks:bool ->
- ?include_paths:string list ->
+ include_paths:string list ->
?clean_baseuri:bool ->
GrafiteTypes.status ref -> Ulexing.lexbuf ->
(GrafiteTypes.status -> GrafiteParser.statement -> unit) ->
val eval_from_stream_greedy:
?do_heavy_checks:bool ->
- ?include_paths:string list ->
+ include_paths:string list ->
?clean_baseuri:bool ->
GrafiteTypes.status ref-> Ulexing.lexbuf ->
(GrafiteTypes.status -> GrafiteParser.statement -> unit) ->
let ask_and_save_moo_if_needed parent fname status =
let basedir = Helm_registry.get "matita.basedir" in
+ let baseuri = GrafiteParserMisc.baseuri_of_script ~include_paths:[] fname in
+ let moo_fname = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
let save () =
- let moo_fname = GrafiteMisc.obj_file_of_script ~basedir fname in
- let metadata_fname = GrafiteMisc.metadata_file_of_script ~basedir fname in
+ let metadata_fname= LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in
GrafiteMarshal.save_moo moo_fname status.GrafiteTypes.moo_content_rev;
LibraryNoDb.save_metadata metadata_fname status.GrafiteTypes.metadata
in
status.GrafiteTypes.proof_status = GrafiteTypes.No_proof
then
begin
- let mooname = GrafiteMisc.obj_file_of_script ~basedir fname in
let rc =
MatitaGtkMisc.ask_confirmation
~title:"A .moo can be generated"
~message:(Printf.sprintf
"%s can be generated for %s.\n<i>Should I generate it?</i>"
- (Filename.basename mooname) (Filename.basename fname))
+ (Filename.basename moo_fname) (Filename.basename fname))
~parent ()
in
let b =
wants [ConfigurationFile] init_status;
if not (already_configured [Notation] init_status) then
begin
- CicNotation.load_notation BuildTimeConf.core_notation_script;
+ CicNotation2.load_notation BuildTimeConf.core_notation_script;
Notation::init_status
end
else
(* | Incomplete_proof { stack = stack }
when not (List.mem user_goal (Continuationals.head_goals stack)) ->
let status =
- MatitaEngine.eval_ast ~include_paths:include_
+ MatitaEngine.eval_ast
~do_heavy_checks:true status (goal_ast user_goal)
in
let initial_space = if initial_space = "" then "\n" else initial_space
| _ -> initial_space,status,[] in
let new_status =
GrafiteEngine.eval_ast
+ ~baseuri_of_script:(GrafiteParserMisc.baseuri_of_script ~include_paths:include_)
~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
~disambiguate_command:GrafiteDisambiguate.disambiguate_command
- ~include_paths:include_ ~do_heavy_checks:true new_status st
+ ~do_heavy_checks:true new_status st
in
let new_aliases =
match ex with
try
eval_with_engine guistuff status user_goal parsed_text st
with
- | GrafiteEngine.UnableToInclude what
+ | GrafiteParserMisc.UnableToInclude what
| GrafiteEngine.IncludedFileNotCompiled what as exc ->
let compile_needed_and_go_on d =
let target = what in
in
let new_status =
GrafiteEngine.eval_ast
+ ~baseuri_of_script:(fun _ -> assert false)
~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
~disambiguate_command:GrafiteDisambiguate.disambiguate_command
status ast in
match ex with
| TA.Command (loc, _) | TA.Tactical (loc, _, _) ->
(try
- (match GrafiteMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
+ (match GrafiteParserMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
| None -> ()
| Some u ->
if not (GrafiteMisc.is_empty u) then
LibraryClean.clean_baseuris ~basedir [u]
| `NO -> ()
| `CANCEL -> raise MatitaTypes.Cancel);
- eval_with_engine
- guistuff 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 guistuff status user_goal unparsed_text parsed_text script mac
let go () =
Helm_registry.load_from BuildTimeConf.matita_conf;
- CicNotation.load_notation BuildTimeConf.core_notation_script;
+ CicNotation2.load_notation BuildTimeConf.core_notation_script;
Http_getter.init ();
MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
LibraryDb.create_owner_environment ();
Ulexing.from_utf8_channel
(match fname with
| "stdin" -> stdin
- | fname -> open_in fname)
+ | fname -> open_in fname) in
+ let include_paths =
+ Helm_registry.get_list Helm_registry.string "matita.includes"
in
run_script is
- (MatitaEngine.eval_from_stream
- ~include_paths:(Helm_registry.get_list Helm_registry.string
- "matita.includes")
+ (MatitaEngine.eval_from_stream ~include_paths
~clean_baseuri:(not (Helm_registry.get_bool "matita.preserve")));
let elapsed = Unix.time () -. time in
let tm = Unix.gmtime elapsed in
else
begin
let basedir = Helm_registry.get "matita.basedir" in
- let moo_fname = GrafiteMisc.obj_file_of_script ~basedir fname in
- let metadata_fname = GrafiteMisc.metadata_file_of_script ~basedir fname in
+ let baseuri = GrafiteParserMisc.baseuri_of_script ~include_paths fname in
+ let moo_fname = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
+ let metadata_fname = LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in
GrafiteMarshal.save_moo moo_fname moo_content_rev;
LibraryNoDb.save_metadata metadata_fname metadata;
HLog.message
let main () =
let _ = MatitaInit.initialize_all () in
- let uris_to_remove = ref [] in
- let files_to_remove = ref [] in
let basedir = Helm_registry.get "matita.basedir" in
- (match Helm_registry.get_list Helm_registry.string "matita.args" with
+ match Helm_registry.get_list Helm_registry.string "matita.args" with
| [ "all" ] ->
LibraryDb.clean_owner_environment ();
let xmldir = basedir ^ "/xml" in
exit 0
| [] -> MatitaInit.die_usage ()
| files ->
- List.iter
- (fun suri ->
+ let uris_to_remove =
+ List.fold_left
+ (fun uris_to_remove suri ->
let uri =
try
UM.buri_of_uri (UM.uri_of_string suri)
with UM.IllFormedUri _ ->
- files_to_remove := suri :: !files_to_remove;
- let u = GrafiteMisc.baseuri_of_file suri in
+ let u =
+ GrafiteParserMisc.baseuri_of_script ~include_paths:[] suri in
if String.length u < 5 || String.sub u 0 5 <> "cic:/" then begin
HLog.error (sprintf "File %s defines a bad baseuri: %s"
suri u);
end else
u
in
- uris_to_remove := uri :: !uris_to_remove)
- files);
- LibraryClean.clean_baseuris ~basedir !uris_to_remove;
- let moos =
- List.map (GrafiteMisc.obj_file_of_script ~basedir) !files_to_remove
- in
- List.iter HExtlib.safe_remove moos
-
+ uri::uris_to_remove) [] files
+ in
+ LibraryClean.clean_baseuris ~basedir uris_to_remove
let buri alias = U.buri_of_uri (U.uri_of_string alias) in
let resolve alias current_buri =
let buri = buri alias in
- if buri <> current_buri then Some buri else None
- in
- let find path =
- let rec aux = function
- | [] -> close_in (open_in path); path
- | p :: tl ->
- try
- close_in (open_in (p ^ "/" ^ path)); p ^ "/" ^ path
- with Sys_error _ -> aux tl
- in
- let paths = Helm_registry.get_list Helm_registry.string "matita.includes" in
- try
- aux paths
- with Sys_error _ as exc ->
- HLog.error ("Unable to read " ^ path);
- HLog.error ("opts.include_paths was " ^ String.concat ":" paths);
- raise exc
- in
+ if buri <> current_buri then Some buri else None in
+ let include_paths =
+ Helm_registry.get_list Helm_registry.string "matita.includes" in
MatitaInit.load_configuration_file ();
MatitaInit.parse_cmdline ();
let basedir = Helm_registry.get "matita.basedir" in
List.iter
- (fun file ->
- let ic = open_in file in
+ (fun ma_file ->
+ let ic = open_in ma_file in
let istream = Ulexing.from_utf8_channel ic in
let dependencies = GrafiteParser.parse_dependencies istream in
close_in ic;
List.iter
- (function
- | GrafiteAst.UriDep uri ->
+ (function
+ | GrafiteAst.UriDep uri ->
let uri = UriManager.string_of_uri uri in
- Hashtbl.add uri_deps file uri
- | GrafiteAst.BaseuriDep uri ->
+ Hashtbl.add uri_deps ma_file uri
+ | GrafiteAst.BaseuriDep uri ->
let uri = Http_getter_misc.strip_trailing_slash uri in
- Hashtbl.add baseuri_of file uri
- | GrafiteAst.IncludeDep path ->
+ Hashtbl.add baseuri_of ma_file uri
+ | GrafiteAst.IncludeDep path ->
try
- let ma_file = if path <> "coq.ma" then find path else path in
- let moo_file = GrafiteMisc.obj_file_of_script ~basedir ma_file in
- Hashtbl.add include_deps file moo_file
+ let baseuri =
+ GrafiteParserMisc.baseuri_of_script ~include_paths path in
+ let moo_file = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
+ Hashtbl.add include_deps ma_file moo_file
with Sys_error _ ->
HLog.warn
- ("Unable to find " ^ path ^ " that is included in " ^ file))
- dependencies)
- (Helm_registry.get_list Helm_registry.string "matita.args");
+ ("Unable to find " ^ path ^ " that is included in " ^ ma_file)
+ ) dependencies
+ ) (Helm_registry.get_list Helm_registry.string "matita.args");
Hashtbl.iter
(fun file alias ->
let dep = resolve alias (Hashtbl.find baseuri_of file) in
(LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri:u))
uri_deps;
List.iter
- (fun file ->
- let deps = Hashtbl.find_all include_deps file in
+ (fun ma_file ->
+ let deps = Hashtbl.find_all include_deps ma_file in
let deps = List.fast_sort Pervasives.compare deps in
let deps = HExtlib.list_uniq deps in
- let deps = file :: deps in
- let moo = GrafiteMisc.obj_file_of_script ~basedir file in
+ let deps = ma_file :: deps in
+ let baseuri = Hashtbl.find baseuri_of ma_file in
+ let moo = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
Printf.printf "%s: %s\n" moo (String.concat " " deps);
- Printf.printf "%s: %s\n" (Pcre.replace ~pat:"ma$" ~templ:"mo" file) moo)
+ Printf.printf "%s: %s\n" (Pcre.replace ~pat:"ma$" ~templ:"mo" ma_file) moo)
(Helm_registry.get_list Helm_registry.string "matita.args")
projects / helm.git / commitdiff