(* log *)
HLog.set_log_callback self#console#log_callback;
GtkSignal.user_handler :=
- (fun exn ->
+ (function
+ | MatitaScript.ActionCancelled -> ()
+ | exn ->
if not (Helm_registry.get_bool "matita.debug") then
let floc, msg = MatitaExcPp.to_string exn in
begin
(** raised when one of the script margins (top or bottom) is reached *)
exception Margin
exception NoUnfinishedProof
+exception ActionCancelled
let safe_substring s i j =
try String.sub s i j with Invalid_argument _ -> assert false
in
res,parsed_text_length
-let eval_with_engine
- guistuff lexicon_status grafite_status user_goal parsed_text st
-=
- try
- eval_with_engine guistuff lexicon_status grafite_status user_goal parsed_text
- st
+let wrap_with_developments guistuff f arg =
+ try
+ f arg
with
| DependenciesParser.UnableToInclude what
+ | LexiconEngine.IncludedFileNotCompiled what
| GrafiteEngine.IncludedFileNotCompiled what as exc ->
let compile_needed_and_go_on d =
- let target = what in
+ let target = Pcre.replace ~pat:"lexicon$" ~templ:"moo" what in
let refresh_cb () =
while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
in
if not(MatitamakeLib.build_development_in_bg ~target refresh_cb d) then
raise exc
else
- eval_with_engine guistuff lexicon_status grafite_status user_goal
- parsed_text st
+ f arg
in
- let do_nothing () = [], 0 in
+ let do_nothing () = raise ActionCancelled in
let handle_with_devel d =
let name = MatitamakeLib.name_for_development d in
let title = "Unable to include " ^ what in
| None -> handle_without_devel (Some f)
| Some d -> handle_with_devel d
;;
+
+let eval_with_engine
+ guistuff lexicon_status grafite_status user_goal parsed_text st
+=
+ wrap_with_developments guistuff
+ (eval_with_engine
+ guistuff lexicon_status grafite_status user_goal parsed_text) st
+;;
let pp_eager_statement_ast =
GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
match statement with
| `Raw text ->
if Pcre.pmatch ~rex:only_dust_RE text then raise Margin;
- GrafiteParser.parse_statement (Ulexing.from_utf8_string text)
- ~include_paths lexicon_status, text
+ let ast =
+ wrap_with_developments guistuff
+ (GrafiteParser.parse_statement
+ (Ulexing.from_utf8_string text) ~include_paths) lexicon_status
+ in
+ ast, text
| `Ast (st, text) -> (lexicon_status, st), text
in
let text_of_loc loc =
method eos =
let s = self#getFuture in
- let rec is_there_and_executable lexicon_status s =
+ let rec is_there_only_comments lexicon_status s =
if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
let lexicon_status,st =
GrafiteParser.parse_statement (Ulexing.from_utf8_string s)
~include_paths lexicon_status
in
match st with
- GrafiteParser.LNone loc
| GrafiteParser.LSome (GrafiteAst.Comment (loc,_)) ->
let parsed_text_length = snd (HExtlib.loc_of_floc loc) in
let remain_len = String.length s - parsed_text_length in
let next = String.sub s parsed_text_length remain_len in
- is_there_and_executable lexicon_status next
- | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) -> false
+ is_there_only_comments lexicon_status next
+ | GrafiteParser.LNone _
+ | GrafiteParser.LSome (GrafiteAst.Executable _) -> false
in
try
- is_there_and_executable self#lexicon_status s
+ is_there_only_comments self#lexicon_status s
with
| CicNotationParser.Parse_error _ -> false
| Margin | End_of_file -> true
*)
exception NoUnfinishedProof
+exception ActionCancelled
class type script =
object
let eval_coercion status ~add_composites uri =
let basedir = Helm_registry.get "matita.basedir" in
let status,compounds =
+ prerr_endline "evaluating a coercion command";
GrafiteSync.add_coercion ~basedir ~add_composites status uri in
let moo_content = coercion_moo_statement_of uri in
let status = GrafiteTypes.add_moo_content [moo_content] status in
None)
lemmas)
in
+ prerr_endline "actual coercions:";
List.iter
(fun u -> prerr_endline (UriManager.string_of_uri u))
coercions;
- let status = GrafiteTypes.add_moo_content moo_content status in
- let basedir = Helm_registry.get "matita.basedir" in
- List.fold_left
- (fun (status,lemmas) uri ->
- let status,new_lemmas =
- GrafiteSync.add_coercion ~basedir ~add_composites:true status uri
- in
- status,new_lemmas@lemmas
- ) (status,[]) coercions
+ let status = GrafiteTypes.add_moo_content moo_content status in
+ {status with
+ GrafiteTypes.coercions = coercions @ status.GrafiteTypes.coercions},
+ lemmas
let add_obj uri obj status =
let basedir = Helm_registry.get "matita.basedir" in
* http://helm.cs.unibo.it/
*)
+exception IncludedFileNotCompiled of string
type status = {
aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
C.Lambda (name, aux so, aux dest)
| C.LetIn (name,so,dest) ->
C.LetIn (name, aux so, aux dest)
- | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) when
+ | Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ] when
CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
let source_carr = CoercGraph.source_of c2 in
let tgt_carr = CoercGraph.target_of c1 in
in
(* store that composite_uris are related to uri. the first component is the
* stuff in the DB while the second is stuff for remove_obj *)
+ prerr_endline ("aggiungo: " ^ string_of_bool add_composites ^ UriManager.string_of_uri uri);
+ List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
+ composite_uris;
UriManager.UriHashtbl.add coercion_hashtbl uri
(composite_uris,if add_composites then composite_uris else []);
lemmas
let (composites_in_db, composites_in_lib) =
UriManager.UriHashtbl.find coercion_hashtbl uri
in
+ prerr_endline ("removing: " ^UriManager.string_of_uri uri);
+ List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
+ composites_in_db;
UriManager.UriHashtbl.remove coercion_hashtbl uri;
CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq uri u);
(* remove from the DB *)
CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
let attrs = [`Class `Projection; `Generated] in
let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
-
add_single_obj ~basedir uri obj;
let composites =
if coercion then
include ../../Makefile.common
-all:saturate
-opt:saturate.opt
+all $(PACKAGE).cma :saturate
+opt $(PACKAGE).cmxa:saturate.opt
saturate: saturate_main.ml $(LIBRARIES)
$(OCAMLC) $(LOCALLINKOPTS) -thread -linkpkg -o $@ $<
projects / helm.git / commitdiff