X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaScript.ml;h=188726d9510879720ff984782cd5d8e26fe558d6;hb=b5619c04607ec92594e7645847409c351129709b;hp=a94d8aecf90aa932f9863c59247b690560bf92e0;hpb=0b79601e4c529cacbba2b64f99f3548df412f254;p=helm.git diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index a94d8aecf..188726d95 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -36,6 +36,7 @@ let debug_print = if debug then prerr_endline else ignore (** 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 @@ -80,8 +81,6 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal = let module TAPp = GrafiteAstPp in let parsed_text_length = String.length parsed_text in - let loc, ex = - match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false in let initial_space,parsed_text = try let pieces = Pcre.extract ~rex:heading_nl_RE' parsed_text in @@ -91,7 +90,9 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal let inital_space,new_grafite_status,new_lexicon_status,new_status_and_text_list' = (* the code commented out adds the "select" command if needed *) initial_space,grafite_status,lexicon_status,[] in -(* match grafite_status.proof_status with +(* let loc, ex = + match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false in + match grafite_status.proof_status with | Incomplete_proof { stack = stack } when not (List.mem user_goal (Continuationals.head_goals stack)) -> let grafite_status = @@ -140,27 +141,24 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal 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 @@ -198,6 +196,14 @@ let eval_with_engine | 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 @@ -352,8 +358,12 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status 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 = @@ -499,7 +509,9 @@ object (self) bottom) and we will face a macro *) match self#grafite_status.proof_status with Incomplete_proof p -> - userGoal <- Some (Continuationals.Stack.find_goal p.stack) + userGoal <- + (try Some (Continuationals.Stack.find_goal p.stack) + with Failure _ -> None) | _ -> userGoal <- None method private _retract offset lexicon_status grafite_status new_statements @@ -755,9 +767,8 @@ object (self) method proofContext = match userGoal with - None -> assert false - | Some n -> - GrafiteTypes.get_proof_context self#grafite_status n + None -> [] + | Some n -> GrafiteTypes.get_proof_context self#grafite_status n method proofConclusion = match userGoal with @@ -771,23 +782,23 @@ object (self) 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