else
s
-let empty_mathml () =
+let empty_mathml = lazy (
DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.mathml_ns)
- ~qualifiedName:(Gdome.domString "math") ~doctype:None
+ ~qualifiedName:(Gdome.domString "math") ~doctype:None)
-let empty_boxml () =
+let empty_boxml = lazy (
DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.boxml_ns)
- ~qualifiedName:(Gdome.domString "box") ~doctype:None
+ ~qualifiedName:(Gdome.domString "box") ~doctype:None)
+
+let closed_goal_mathml = lazy (
+ DomMisc.domImpl#createDocumentFromURI ~uri:BuildTimeConf.closed_xml ())
exception History_failure
let instance = lazy (f ()) in
fun () -> Lazy.force instance
-let get_proof_status status =
+let get_current_proof status =
match status.proof_status with
- | Incomplete_proof s -> s
+ | Incomplete_proof { proof = p } -> p
| _ -> statement_error "no ongoing proof"
let get_proof_metasenv status =
match status.proof_status with
| No_proof -> []
- | Incomplete_proof ((_, metasenv, _, _), _) -> metasenv
- | Proof (_, metasenv, _, _) -> metasenv
- | Intermediate m -> m
+ | Proof (_, metasenv, _, _)
+ | Incomplete_proof { proof = (_, metasenv, _, _) }
+ | Intermediate metasenv ->
+ metasenv
-let get_proof_context status =
+let get_proof_context status goal =
match status.proof_status with
- | Incomplete_proof ((_, metasenv, _, _), goal) ->
+ | Incomplete_proof { proof = (_, metasenv, _, _) } ->
let (_, context, _) = CicUtil.lookup_meta goal metasenv in
context
| _ -> []
-let get_proof_conclusion status =
+let get_proof_conclusion status goal =
match status.proof_status with
- | Incomplete_proof ((_, metasenv, _, _), goal) ->
+ | Incomplete_proof { proof = (_, metasenv, _, _) } ->
let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in
conclusion
| _ -> statement_error "no ongoing proof"
+
+let get_stack status =
+ 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
+ | Incomplete_proof p ->
+ { status with proof_status = Incomplete_proof { p with stack = stack } }
+ | Proof _ ->
+ assert (Continuationals.Stack.is_empty stack);
+ status
+ | _ -> assert false
let qualify status name = get_string_option status "baseuri" ^ "/" ^ name