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
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 _ -> ()
+;;
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} *)
(* 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
| 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
{
GrafiteTypes.moo_content_rev = [];
proof_status = GrafiteTypes.No_proof;
- options = GrafiteTypes.no_options;
+(* options = GrafiteTypes.no_options; *)
objects = [];
coercions = [];
universe = Universe.empty;
(* 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;
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 =
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";
| Proof _ -> "proof\n"
| Intermediate _ -> "Intermediate\n");
HLog.message "status.options\n";
+(* REMOVEME
StringMap.iter (fun k v ->
let v =
match v with
| 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
| 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 *)
(** 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
-exception UnableToQualify
+exception NoRootFor of string
let find_root path =
let paths = List.rev (Str.split (Str.regexp "/") path) in
| [] -> ["/"]
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
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
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
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 =
-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:
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"
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/test/".
-
(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: *)
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.\n<i>Should I generate it?</i>"
- (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
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
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
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 ()
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 = []
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 :> <check_widgets: unit -> unit>) in
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 ()
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
| `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
| 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 ();
(s ())#template ();
source_view#source_buffer#end_not_undoable_action ();
disableSave ();
- script_fname <- None
+ (s ())#assignFileName None
in
let cursor () =
source_buffer#place_cursor
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;
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
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 ();
end
else
begin
- script#assignFileName file;
+ script#assignFileName (Some file);
let content =
if Sys.file_exists file then file
else BuildTimeConf.script_template
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
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
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";
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.
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 ());
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;
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
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;
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
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
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
(** @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 *)
(** end of script, true if the whole script has been executed *)
method eos: bool
+ method bos: bool
(** misc *)
method clean_dirty_lock: unit
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
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
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
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
;;
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
+++ /dev/null
-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@
+++ /dev/null
-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)
projects / helm.git / commitdiff