Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

code cleanup
ci/woodpecker/push/build Pipeline was successful Details

This commit is contained in:
Burkhart Wolff 2023-03-24 12:59:54 +01:00
parent 63c2acfece
commit 0834f938a9
1 changed files with 10 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
Isabelle_DOF-Unit-Tests/TestKit.thy
View File

@ -26,8 +26,7 @@ keywords "text-" "text-latex" :: document_body
begin
section\<open>Testing Commands (exec-catch-verify - versions of std commands)\<close>
section\<open>Testing Commands (exec-catch-verify - versions of DOF commands)\<close>
ML\<open>
@ -102,15 +101,14 @@ fun output_document2 state markdown txt =
in Document_Output.output_document ctxt markdown txt end;
fun document_command2 markdown (loc, txt) =
Toplevel.keep (fn state =>
(case loc of
let fun doc2 state = (case loc of
NONE => ignore (output_document2 state markdown txt)
| SOME (_, pos) =>(ISA_core.err
"Illegal target specification -- not a theory context"
pos)))
o
Toplevel.present_local_theory loc (fn state => (output_document2 state markdown txt));
pos))
fun out2 state = output_document2 state markdown txt
in Toplevel.keep doc2 o Toplevel.present_local_theory loc out2
end
fun gen_enriched_document_command3 assert name body trans at md (margs, src_list) thy
= (gen_enriched_document_command2 name body trans at md (margs, src_list) thy)
@ -149,19 +147,12 @@ val _ =
then (writeln ("Correct error: "^msg^": reported.");thy)
else error"Wrong error reported")
in Outer_Syntax.command \<^command_keyword>\<open>declare_reference-assert-error\<close>
"declare document reference"
(ODL_Meta_Args_Parser.attributes -- Parse.document_source
>> (Toplevel.theory o create_and_check_docitem))
"declare document reference"
(ODL_Meta_Args_Parser.attributes -- Parse.document_source
>> (Toplevel.theory o create_and_check_docitem))
end;
(* fun pass_trans_to_value_cmd args ((name, modes), t) trans =
let val pos = Toplevel.pos_of trans
in
trans |> Toplevel.theory (value_cmd {assert=false} args name modes t @{here})
end
*)
val _ =
let fun pass_trans_to_value_cmd (args, (((name, modes), t),src)) trans =
(Value_Command.value_cmd {assert=false} args name modes t @{here} trans
@ -184,10 +175,9 @@ val _ =
\<close>
(* auto-tests *)
(* a little auto-test *)
text-latex\<open>dfg\<close>
text-assert-error[aaaa::A]\<open> @{A \<open>sdf\<close>}\<close>\<open>reference ontologically inconsistent\<close>