| GrafiteAst.ApplyP (_, term) -> Tactics.applyP term
| GrafiteAst.ApplyS (_, term, params) ->
Tactics.applyS ~term ~params ~dbd:(LibraryDb.instance ())
- ~automation_cache:status.GrafiteTypes.automation_cache
+ ~automation_cache:status#automation_cache
| GrafiteAst.Assumption _ -> Tactics.assumption
| GrafiteAst.AutoBatch (_,params) ->
Tactics.auto ~params ~dbd:(LibraryDb.instance ())
- ~automation_cache:status.GrafiteTypes.automation_cache
+ ~automation_cache:status#automation_cache
| GrafiteAst.Cases (_, what, pattern, (howmany, names)) ->
Tactics.cases_intros ?howmany ~mk_fresh_name_callback:(namer_of names)
~pattern what
| GrafiteAst.Demodulate (_, params) ->
Tactics.demodulate
~dbd:(LibraryDb.instance ()) ~params
- ~automation_cache:status.GrafiteTypes.automation_cache
+ ~automation_cache:status#automation_cache
| GrafiteAst.Destruct (_,xterms) -> Tactics.destruct xterms
| GrafiteAst.Elim (_, what, using, pattern, (depth, names)) ->
Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
| GrafiteAst.Suppose (_, t, id, t1) -> Declarative.suppose t id t1
| GrafiteAst.By_just_we_proved (_, just, ty, id, t1) ->
Declarative.by_just_we_proved ~dbd:(LibraryDb.instance())
- ~automation_cache:status.GrafiteTypes.automation_cache just ty id t1
+ ~automation_cache:status#automation_cache just ty id t1
| GrafiteAst.We_need_to_prove (_, t, id, t2) ->
Declarative.we_need_to_prove t id t2
| GrafiteAst.Bydone (_, t) ->
Declarative.bydone ~dbd:(LibraryDb.instance())
- ~automation_cache:status.GrafiteTypes.automation_cache t
+ ~automation_cache:status#automation_cache t
| GrafiteAst.We_proceed_by_cases_on (_, t, t1) ->
Declarative.we_proceed_by_cases_on t t1
| GrafiteAst.We_proceed_by_induction_on (_, t, t1) ->
| GrafiteAst.Thesisbecomes (_, t) -> Declarative.thesisbecomes t
| GrafiteAst.ExistsElim (_, just, id1, t1, id2, t2) ->
Declarative.existselim ~dbd:(LibraryDb.instance())
- ~automation_cache:status.GrafiteTypes.automation_cache just id1 t1 id2 t2
+ ~automation_cache:status#automation_cache just id1 t1 id2 t2
| GrafiteAst.Case (_,id,params) -> Declarative.case id params
| GrafiteAst.AndElim(_,just,id1,t1,id2,t2) ->
Declarative.andelim ~dbd:(LibraryDb.instance ())
- ~automation_cache:status.GrafiteTypes.automation_cache just id1 t1 id2 t2
+ ~automation_cache:status#automation_cache just id1 t1 id2 t2
| GrafiteAst.RewritingStep (_,termine,t1,t2,cont) ->
Declarative.rewritingstep ~dbd:(LibraryDb.instance ())
- ~automation_cache:status.GrafiteTypes.automation_cache termine t1 t2 cont
+ ~automation_cache:status#automation_cache termine t1 t2 cont
let classify_tactic tactic =
match tactic with
proof', opened_goals
in
let incomplete_proof =
- match status.GrafiteTypes.proof_status with
+ match status#proof_status with
| GrafiteTypes.Incomplete_proof p -> p
| _ -> assert false
in
- { status with GrafiteTypes.proof_status =
- GrafiteTypes.Incomplete_proof
- { incomplete_proof with GrafiteTypes.proof = proof } },
+ status#set_proof_status
+ (GrafiteTypes.Incomplete_proof
+ { incomplete_proof with GrafiteTypes.proof = proof }),
opened_goals, closed_goals
let apply_atomic_tactical ~disambiguate_tactic ~patch (text,prefix_len,tactic) (status, goal) =
proof', opened_goals
in
let incomplete_proof =
- match status.GrafiteTypes.proof_status with
+ match status#proof_status with
| GrafiteTypes.Incomplete_proof p -> p
| _ -> assert false
in
- { status with GrafiteTypes.proof_status =
- GrafiteTypes.Incomplete_proof
- { incomplete_proof with GrafiteTypes.proof = proof } },
+ status#set_proof_status
+ (GrafiteTypes.Incomplete_proof
+ { incomplete_proof with GrafiteTypes.proof = proof }),
opened_goals, closed_goals
type eval_ast =
{ea_go:
lemmas
in
let status = GrafiteTypes.add_moo_content moo_content status in
- {status with GrafiteTypes.coercions = CoercDb.dump () },
+ status#set_coercions (CoercDb.dump ()),
lemmas
let eval_coercion status ~add_composites uri arity saturations =
let eval_tactical status tac =
let status, _, _ = MatitaTacticals.eval tac (status, ~-1) in
let status = (* is proof completed? *)
- match status.GrafiteTypes.proof_status with
+ match status#proof_status with
| GrafiteTypes.Incomplete_proof
{ GrafiteTypes.stack = stack; proof = proof }
when Continuationals.Stack.is_empty stack ->
- { status with GrafiteTypes.proof_status = GrafiteTypes.Proof proof }
+ status#set_proof_status (GrafiteTypes.Proof proof)
| _ -> status
in
status
match cmd with
| GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
| GrafiteAst.NQed loc ->
- (match status.GrafiteTypes.ng_status with
+ (match status#ng_status with
| GrafiteTypes.ProofMode estatus ->
let uri,height,menv,subst,obj_kind = estatus#obj in
if menv <> [] then
estatus,uri::uris_rev
) (estatus,[]) objs in
let uris = uri::List.rev uris_rev in
- {status with
- GrafiteTypes.ng_status =
- GrafiteTypes.CommandMode (estatus :> NEstatus.status)},`New uris
+ status#set_ng_status
+ (GrafiteTypes.CommandMode (estatus :> NEstatus.status)),`New uris
| _ -> raise (GrafiteTypes.Command_error "Not in proof mode"))
| GrafiteAst.NObj (loc,obj) ->
let estatus =
- match status.GrafiteTypes.ng_status with
+ match status#ng_status with
| GrafiteTypes.ProofMode _ -> assert false
| GrafiteTypes.CommandMode es -> es
in
let uri,height,nmenv,nsubst,nobj = obj in
let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
let status =
- { status with
- GrafiteTypes.ng_status =
- GrafiteTypes.ProofMode
- (subst_metasenv_and_fix_names
- ((new NTacStatus.status obj ninitial_stack)#set_estatus estatus))
- }
+ status#set_ng_status
+ (GrafiteTypes.ProofMode
+ (subst_metasenv_and_fix_names
+ ((new NTacStatus.status obj ninitial_stack)#set_estatus estatus)))
in
(match nmenv with
[] ->
assert false (* TODO: for user input *)
| GrafiteAst.Index (loc,Some key,uri) ->
let universe =
- status.GrafiteTypes.automation_cache.AutomationCache.univ
+ status#automation_cache.AutomationCache.univ
in
let universe = Universe.index universe key (CicUtil.term_of_uri uri) in
let cache = {
- status.GrafiteTypes.automation_cache with AutomationCache.univ = universe }
+ status#automation_cache with AutomationCache.univ = universe }
in
- let status = { status with GrafiteTypes.automation_cache = cache } in
+ let status = status#set_automation_cache cache in
(* debug
let msg =
let candidates = Universe.get_candidates status.GrafiteTypes.universe key in
let status = GrafiteTypes.add_moo_content [cmd] status in
status,`Old []
| GrafiteAst.Select (_,uri) as cmd ->
- if List.mem cmd status.GrafiteTypes.moo_content_rev then status, `Old []
+ if List.mem cmd status#moo_content_rev then status, `Old []
else
let cache =
- AutomationCache.add_term_to_active status.GrafiteTypes.automation_cache
+ AutomationCache.add_term_to_active status#automation_cache
[] [] [] (CicUtil.term_of_uri uri) None
in
- let status = { status with GrafiteTypes.automation_cache = cache } in
+ let status = status#set_automation_cache cache in
let status = GrafiteTypes.add_moo_content [cmd] status in
status, `Old []
| GrafiteAst.Pump (_,steps) ->
let cache =
- AutomationCache.pump status.GrafiteTypes.automation_cache steps
+ AutomationCache.pump status#automation_cache steps
in
- let status = { status with GrafiteTypes.automation_cache = cache } in
+ let status = status#set_automation_cache cache in
status, `Old []
| GrafiteAst.PreferCoercion (loc, coercion) ->
eval_prefer_coercion status coercion
| GrafiteAst.Print (_,_) -> status,`Old []
| GrafiteAst.Qed loc ->
let uri, metasenv, _subst, bo, ty, attrs =
- match status.GrafiteTypes.proof_status with
+ match status#proof_status with
| GrafiteTypes.Proof (Some uri, metasenv, subst, body, ty, attrs) ->
uri, metasenv, subst, body, ty, attrs
| GrafiteTypes.Proof (None, metasenv, subst, body, ty, attrs) ->
let name = UriManager.name_of_uri uri in
let obj = Cic.Constant (name,Some (Lazy.force bo),ty,[],attrs) in
let status, lemmas = add_obj uri obj status in
- {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
+ status#set_proof_status GrafiteTypes.No_proof,
(*CSC: I throw away the arities *)
`Old (uri::lemmas)
| GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) ->
let _subst = [] in
let initial_proof = (Some uri, metasenv', _subst, lazy bo, ty, attrs) in
let initial_stack = Continuationals.Stack.of_metasenv metasenv' in
- { status with GrafiteTypes.proof_status =
- GrafiteTypes.Incomplete_proof
- { GrafiteTypes.proof = initial_proof; stack = initial_stack } ;
- },
+ status#set_proof_status
+ (GrafiteTypes.Incomplete_proof
+ { GrafiteTypes.proof = initial_proof; stack = initial_stack }),
`Old []
| _ ->
if metasenv <> [] then
CicMetaSubst.ppmetasenv [] metasenv));
let status, lemmas = add_obj uri obj status in
let status,new_lemmas = add_coercions_of_lemmas lemmas status in
- {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
+ status#set_proof_status GrafiteTypes.No_proof,
`Old (uri::new_lemmas@lemmas)
in
- match status.GrafiteTypes.proof_status with
+ match status#proof_status with
GrafiteTypes.Intermediate _ ->
- {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},uris
+ status#set_proof_status GrafiteTypes.No_proof,uris
| _ -> status,uris
} and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command
eval_tactical status
(punctuation_tactical_of_ast (text,prefix_len,punct)),`Old []
| GrafiteAst.NTactic (_(*loc*), tacl) ->
- (match status.GrafiteTypes.ng_status with
+ (match status#ng_status with
| GrafiteTypes.CommandMode _ -> assert false
| GrafiteTypes.ProofMode nstatus ->
let nstatus =
subst_metasenv_and_fix_names nstatus)
nstatus tacl
in
- { status with GrafiteTypes.ng_status= GrafiteTypes.ProofMode nstatus },
+ status#set_ng_status (GrafiteTypes.ProofMode nstatus),
`New [])
| GrafiteAst.NonPunctuationTactical (_, tac, punct) ->
let status =
in
let automation_cache,status =
List.fold_left add_to_universe
- (status.GrafiteTypes.automation_cache,status)
+ (status#automation_cache,status)
uris_to_index
in
- {status with
- GrafiteTypes.objects = uri :: lemmas @ status.GrafiteTypes.objects;
- GrafiteTypes.automation_cache = automation_cache},
- lemmas
+ (status
+ #set_objects (uri :: lemmas @ status#objects))
+ #set_automation_cache automation_cache,
+ lemmas
let add_coercion ~pack_coercion_obj ~add_composites status uri arity
saturations baseuri
LibrarySync.add_coercion ~add_composites ~pack_coercion_obj
uri arity saturations baseuri in
let status =
- { status with GrafiteTypes.coercions = CoercDb.dump () ;
- objects = lemmas @ status.GrafiteTypes.objects;
- }
+ (status
+ #set_coercions (CoercDb.dump ())) ;
+ #set_objects (lemmas @ status#objects)
in
let estatus =
NCicCoercion.index_old_db (CoercDb.dump ()) (GrafiteTypes.get_estatus status)
let status = GrafiteTypes.set_estatus estatus status in
status, lemmas
-let prefer_coercion s u =
+let prefer_coercion status u =
CoercDb.prefer u;
- { s with GrafiteTypes.coercions = CoercDb.dump () }
+ status#set_coercions (CoercDb.dump ())
(** @return l2 \ l1 *)
let uri_list_diff l2 l1 =
let time_travel ~present ~past =
let objs_to_remove =
- uri_list_diff present.GrafiteTypes.objects past.GrafiteTypes.objects in
+ uri_list_diff present#objects past#objects in
List.iter LibrarySync.remove_obj objs_to_remove;
- CoercDb.restore past.GrafiteTypes.coercions;
+ CoercDb.restore past#coercions;
NCicLibrary.time_travel (GrafiteTypes.get_estatus past)
;;
-let initial_status lexicon_status baseuri = {
- GrafiteTypes.moo_content_rev = [];
- proof_status = GrafiteTypes.No_proof;
- objects = [];
- coercions = CoercDb.empty_coerc_db;
- automation_cache = AutomationCache.empty ();
- baseuri = baseuri;
- ng_status = GrafiteTypes.CommandMode (new NEstatus.status)
-}
-
+let initial_status lexicon_status baseuri =
+ new GrafiteTypes.status [] GrafiteTypes.No_proof []
+ CoercDb.empty_coerc_db (AutomationCache.empty ())
+ baseuri (GrafiteTypes.CommandMode (new NEstatus.status))
+;;
let init baseuri =
CoercDb.restore CoercDb.empty_coerc_db;
| ProofMode of NTacStatus.tac_status
| CommandMode of NEstatus.status
-type status = {
- moo_content_rev: GrafiteMarshal.moo;
- proof_status: proof_status;
- objects: UriManager.uri list;
- coercions: CoercDb.coerc_db;
- automation_cache:AutomationCache.cache;
- baseuri: string;
- ng_status: ng_status;
-}
+class status =
+ fun (mcr : GrafiteMarshal.moo) (ps : proof_status) (o : UriManager.uri list)
+ (c : CoercDb.coerc_db) (ac : AutomationCache.cache) (b : string)
+ (ns : ng_status)
+ ->
+ object
+ val moo_content_rev = mcr
+ val proof_status = ps
+ val objects = o
+ val coercions = c
+ val automation_cache = ac
+ val baseuri = b
+ val ng_status = ns
+ method moo_content_rev = moo_content_rev
+ method set_moo_content_rev v = {< moo_content_rev = v >}
+ method proof_status = proof_status
+ method set_proof_status v = {< proof_status = v >}
+ method objects = objects
+ method set_objects v = {< objects = v >}
+ method coercions = coercions
+ method set_coercions v = {< coercions = v >}
+ method automation_cache = automation_cache
+ method set_automation_cache v = {< automation_cache = v >}
+ method baseuri = baseuri
+ method set_baseuri v = {< baseuri = v >}
+ method ng_status = ng_status;
+ method set_ng_status v = {< ng_status = v >}
+ end
let get_estatus x =
- match x.ng_status with
+ match x#ng_status with
| ProofMode t -> (t :> NEstatus.status)
| CommandMode e -> e
;;
let set_estatus e x =
- { x with ng_status =
- match x.ng_status with
+ x#set_ng_status
+ (match x#ng_status with
ProofMode t -> ProofMode t#set_estatus e
- | CommandMode _ -> CommandMode e}
+ | CommandMode _ -> CommandMode e)
;;
let get_current_proof status =
- match status.proof_status with
+ match status#proof_status with
| Incomplete_proof { proof = p } -> p
| Proof p -> p
| _ -> raise (Statement_error "no ongoing proof")
let get_proof_metasenv status =
- match status.proof_status with
+ match status#proof_status with
| No_proof -> []
| Proof (_, metasenv, _, _, _, _)
| Incomplete_proof { proof = (_, metasenv, _, _, _, _) }
metasenv
let get_stack status =
- match status.proof_status with
+ match status#proof_status with
| Incomplete_proof p -> p.stack
| Proof _ -> Continuationals.Stack.empty
| _ -> assert false
let set_stack stack status =
- match status.proof_status with
+ match status#proof_status with
| Incomplete_proof p ->
- { status with proof_status = Incomplete_proof { p with stack = stack } }
+ status#set_proof_status (Incomplete_proof { p with stack = stack })
| Proof _ ->
assert (Continuationals.Stack.is_empty stack);
status
let set_metasenv metasenv status =
let proof_status =
- match status.proof_status with
+ match status#proof_status with
| No_proof -> Intermediate metasenv
| Incomplete_proof ({ proof = (uri, _, subst, proof, ty, attrs) } as incomplete_proof) ->
Incomplete_proof
| Intermediate _ -> Intermediate metasenv
| Proof (_, metasenv', _, _, _, _) ->
assert (metasenv = metasenv');
- status.proof_status
+ status#proof_status
in
- { status with proof_status = proof_status }
+ status#set_proof_status proof_status
let get_proof_context status goal =
- match status.proof_status with
+ match status#proof_status with
| Incomplete_proof { proof = (_, metasenv, _, _, _, _) } ->
let (_, context, _) = CicUtil.lookup_meta goal metasenv in
context
| _ -> []
let get_proof_conclusion status goal =
- match status.proof_status with
+ match status#proof_status with
| Incomplete_proof { proof = (_, metasenv, _, _, _, _) } ->
let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in
conclusion
| _ -> raise (Statement_error "no ongoing proof")
let add_moo_content cmds status =
- let content = status.moo_content_rev in
+ let content = status#moo_content_rev in
let content' =
List.fold_right
(fun cmd acc ->
in
(* prerr_endline ("new moo content: " ^ String.concat " " (List.map
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 set_option status name value =
- let types = [ (* no set options defined! *) ] in
- let ty_and_mangler =
- try List.assoc name types
- with Not_found ->
- command_error (Printf.sprintf "Unknown option \"%s\"" name)
- in
- let value =
- match ty_and_mangler with
- | `String, f -> String (f value)
- | `Int, f ->
- (try
- Int (int_of_string (f value))
- with Failure _ ->
- command_error (Printf.sprintf "Not an integer value \"%s\"" value))
- in
- { status with options = StringMap.add name value status.options }
-
+ status#set_moo_content_rev content'
-let get_string_option status name =
- match get_option status name with
- | String s -> s
- | _ -> raise (Option_error (name, "not a string value"))
-*)
+let get_baseuri status = status#baseuri;;
let dump_status status =
HLog.message "status.aliases:\n";
HLog.message "status.proof_status:";
HLog.message
- (match status.proof_status with
+ (match status#proof_status with
| No_proof -> "no proof\n"
| Incomplete_proof _ -> "incomplete proof\n"
| Proof _ -> "proof\n"
| Intermediate _ -> "Intermediate\n");
HLog.message "status.options\n";
-(* REMOVEME
- StringMap.iter (fun k v ->
- let v =
- match v with
- | String s -> s
- | 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
- (fun u -> HLog.message (UriManager.string_of_uri u)) status.objects
+ (fun u -> HLog.message (UriManager.string_of_uri u)) status#objects
| ProofMode of NTacStatus.tac_status
| CommandMode of NEstatus.status
-type status = {
- moo_content_rev: GrafiteMarshal.moo;
- proof_status: proof_status;
- objects: UriManager.uri list;
- coercions: CoercDb.coerc_db;
- automation_cache:AutomationCache.cache;
- baseuri: string;
- ng_status: ng_status;
-}
+class status :
+ GrafiteMarshal.moo ->
+ proof_status ->
+ UriManager.uri list ->
+ CoercDb.coerc_db ->
+ AutomationCache.cache ->
+ string ->
+ ng_status ->
+ object ('self)
+ method moo_content_rev: GrafiteMarshal.moo
+ method set_moo_content_rev: GrafiteMarshal.moo -> 'self
+ method proof_status: proof_status
+ method set_proof_status: proof_status -> 'self
+ method objects: UriManager.uri list
+ method set_objects: UriManager.uri list -> 'self
+ method coercions: CoercDb.coerc_db
+ method set_coercions: CoercDb.coerc_db -> 'self
+ method automation_cache:AutomationCache.cache
+ method set_automation_cache:AutomationCache.cache -> 'self
+ method baseuri: string
+ method set_baseuri: string -> 'self
+ method ng_status: ng_status
+ method set_ng_status: ng_status -> 'self
+ end
val dump_status : status -> unit
let browser_observer _ = MatitaMathView.refresh_all_browsers () in
let sequents_observer grafite_status =
sequents_viewer#reset;
- match grafite_status.proof_status with
+ match grafite_status#proof_status with
| Incomplete_proof ({ stack = stack } as incomplete_proof) ->
sequents_viewer#load_sequents incomplete_proof;
(try
with Failure _ -> script#setGoal None);
| Proof proof -> sequents_viewer#load_logo_with_qed
| No_proof ->
- (match grafite_status.ng_status with
+ (match grafite_status#ng_status with
ProofMode nstatus ->
sequents_viewer#nload_sequents nstatus;
(try
CicNotationParser.print_l2_pattern;
addDebugItem "dump moo to stderr" (fun _ ->
let grafite_status = (MatitaScript.current ())#grafite_status in
- let moo = grafite_status.moo_content_rev in
+ let moo = grafite_status#moo_content_rev in
List.iter
(fun cmd ->
prerr_endline
HLog.debug
(CicPp.ppterm
(match
- (MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status
+ (MatitaScript.current ())#grafite_status#proof_status
with
| GrafiteTypes.No_proof -> (Cic.Implicit None)
| Incomplete_proof i ->
~map_unicode_to_tex:(Helm_registry.get_bool
"matita.paste_unicode_as_tex")
(match
- (MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status
+ (MatitaScript.current ())#grafite_status#proof_status
with
| GrafiteTypes.No_proof -> assert false
| Incomplete_proof i ->
let script = MatitaScript.current () in
let baseuri = GrafiteTypes.get_baseuri grafite_status in
let no_pstatus =
- grafite_status.GrafiteTypes.proof_status = GrafiteTypes.No_proof
+ grafite_status#proof_status = GrafiteTypes.No_proof
in
match script#bos, script#eos, no_pstatus with
| true, _, _ -> ()
LibraryMisc.lexicon_file_of_baseuri
~must_exist:false ~baseuri ~writable:true
in
- GrafiteMarshal.save_moo moo_fname
- grafite_status.GrafiteTypes.moo_content_rev;
+ GrafiteMarshal.save_moo moo_fname grafite_status#moo_content_rev;
LexiconMarshal.save_lexicon lexicon_fname
(GrafiteTypes.get_estatus grafite_status)#lstatus.LexiconEngine.lexicon_content_rev;
NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
method private home () =
self#_showMath;
- match self#script#grafite_status.proof_status with
+ match self#script#grafite_status#proof_status with
| Proof (uri, metasenv, _subst, bo, ty, attrs) ->
let name = UriManager.name_of_uri (HExtlib.unopt uri) in
let obj =
in
self#_loadObj obj
| _ ->
- match self#script#grafite_status.ng_status with
+ match self#script#grafite_status#ng_status with
ProofMode tstatus -> self#_loadNObj tstatus#obj
| _ -> self#blank ()
in
let t_and_ty = Cic.Cast (term,ty) in
guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
- [({grafite_status with proof_status = No_proof}), parsed_text ],"",
+ [(grafite_status#set_proof_status No_proof), parsed_text ],"",
parsed_text_length
| TA.Check (_,term) ->
let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
let (_,menv,subst,_,_,_), _ =
ProofEngineTypes.apply_tactic
(Auto.auto_tac ~dbd ~params
- ~automation_cache:grafite_status.GrafiteTypes.automation_cache)
+ ~automation_cache:grafite_status#automation_cache)
proof_status
in
let proof_term =
buffer#insert ~iter:(buffer#get_iter_at_mark (`MARK locked_mark)) newtext;
(* here we need to set the Goal in case we are going to cursor (or to
bottom) and we will face a macro *)
- match self#grafite_status.proof_status with
+ match self#grafite_status#proof_status with
Incomplete_proof p ->
userGoal <-
(try Some (Continuationals.Stack.find_goal p.stack)
HLog.error "The script is too big!\n"
method onGoingProof () =
- match self#grafite_status.proof_status with
+ match self#grafite_status#proof_status with
| No_proof | Proof _ -> false
| Incomplete_proof _ -> true
| Intermediate _ -> assert false
| `Do command ->
let str = Ulexing.from_utf8_string command in
let watch_statuses grafite_status =
- match grafite_status.GrafiteTypes.proof_status with
+ match grafite_status#proof_status with
GrafiteTypes.Incomplete_proof
{GrafiteTypes.proof = uri,metasenv,_subst,bo,ty,attrs ;
GrafiteTypes.stack = stack } ->
let proof_status,moo_content_rev,lexicon_content_rev,dump =
match !grafite_status with
| s::_ ->
- s.proof_status, s.moo_content_rev,
+ s#proof_status, s#moo_content_rev,
(GrafiteTypes.get_estatus s)#lstatus.LexiconEngine.lexicon_content_rev,
(GrafiteTypes.get_estatus s)#dump
| _ -> assert false
;;
let get_macro_context = function
- | Some {GrafiteTypes.proof_status = GrafiteTypes.No_proof} -> []
+ | Some status when status#proof_status = GrafiteTypes.No_proof -> []
| Some status ->
let stack = GrafiteTypes.get_stack status in
let goal = Continuationals.Stack.find_goal stack in
in
let elapsed = Unix.time () -. time in
let proof_status,moo_content_rev,lexicon_content_rev =
- grafite_status.proof_status, grafite_status.moo_content_rev,
+ grafite_status#proof_status, grafite_status#moo_content_rev,
(GrafiteTypes.get_estatus grafite_status)#lstatus.LexiconEngine.lexicon_content_rev
in
if proof_status <> GrafiteTypes.No_proof then
projects / helm.git / commitdiff