activated syntactic checks for trimming macros
This commit is contained in:
parent
4c5fc4bc53
commit
4c5aacb39f
|
|
@ -182,7 +182,7 @@ ML\<open>
|
|||
\<close>
|
||||
(*>*)
|
||||
|
||||
text\<open>\<^vs>\<open>-1,0cm\<close>... which we will describe in more detail later. \<close>
|
||||
text\<open>\<^vs>\<open>-1.0cm\<close>... which we will describe in more detail later. \<close>
|
||||
|
||||
text\<open>In a way, anti-quotations implement a kind of
|
||||
literate specification style in text, models, code, proofs, etc., which become alltogether
|
||||
|
|
@ -484,28 +484,28 @@ text\<open>Note, furthermore, that there is a programming API for the HOL-instan
|
|||
operators of the HOL logic specific constructors and destructors:\<close>
|
||||
|
||||
text*[T2::technical]\<open>
|
||||
\<^enum> \<^ML>\<open>HOLogic.boolT : typ\<close> \<^vs>\<open>-0,2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.mk_Trueprop : term -> term\<close>, the embedder of bool to prop fundamental for HOL \<^vs>\<open>-0,2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.dest_Trueprop : term -> term\<close> \<^vs>\<open>-0,2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.Trueprop_conv : conv -> conv\<close> \<^vs>\<open>-0,2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.mk_setT : typ -> typ\<close>, the ML level type constructor set \<^vs>\<open>-0,2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.dest_setT : typ -> typ\<close>, the ML level type destructor for set \<^vs>\<open>-0,2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.Collect_const : typ -> term\<close> \<^vs>\<open>-0,2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.mk_Collect : string * typ * term -> term\<close> \<^vs>\<open>-0,2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.mk_mem : term * term -> term\<close> \<^vs>\<open>-0,2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.dest_mem : term -> term * term\<close> \<^vs>\<open>-0,2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.mk_set : typ -> term list -> term\<close> \<^vs>\<open>-0,2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.conj_intr : Proof.context -> thm -> thm -> thm\<close>, some HOL-level derived-inferences \<^vs>\<open>-0,2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.conj_elim : Proof.context -> thm -> thm * thm\<close> \<^vs>\<open>-0,2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.conj_elims : Proof.context -> thm -> thm list\<close> \<^vs>\<open>-0,2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.conj : term\<close> , some ML level logical constructors \<^vs>\<open>-0,2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.disj : term\<close> \<^vs>\<open>-0,2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.imp : term\<close> \<^vs>\<open>-0,2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.Not : term\<close> \<^vs>\<open>-0,2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.mk_not : term -> term\<close> \<^vs>\<open>-0,2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.mk_conj : term * term -> term\<close> \<^vs>\<open>-0,2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.dest_conj : term -> term list\<close> \<^vs>\<open>-0,2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.conjuncts : term -> term list\<close> \<^vs>\<open>-0,2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.boolT : typ\<close> \<^vs>\<open>-0.2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.mk_Trueprop : term -> term\<close>, the embedder of bool to prop fundamental for HOL \<^vs>\<open>-0.2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.dest_Trueprop : term -> term\<close> \<^vs>\<open>-0.2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.Trueprop_conv : conv -> conv\<close> \<^vs>\<open>-0.2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.mk_setT : typ -> typ\<close>, the ML level type constructor set \<^vs>\<open>-0.2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.dest_setT : typ -> typ\<close>, the ML level type destructor for set \<^vs>\<open>-0.2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.Collect_const : typ -> term\<close> \<^vs>\<open>-0.2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.mk_Collect : string * typ * term -> term\<close> \<^vs>\<open>-0.2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.mk_mem : term * term -> term\<close> \<^vs>\<open>-0.2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.dest_mem : term -> term * term\<close> \<^vs>\<open>-0.2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.mk_set : typ -> term list -> term\<close> \<^vs>\<open>-0.2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.conj_intr : Proof.context -> thm -> thm -> thm\<close>, some HOL-level derived-inferences \<^vs>\<open>-0.2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.conj_elim : Proof.context -> thm -> thm * thm\<close> \<^vs>\<open>-0.2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.conj_elims : Proof.context -> thm -> thm list\<close> \<^vs>\<open>-0.2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.conj : term\<close> , some ML level logical constructors \<^vs>\<open>-0.2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.disj : term\<close> \<^vs>\<open>-0.2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.imp : term\<close> \<^vs>\<open>-0.2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.Not : term\<close> \<^vs>\<open>-0.2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.mk_not : term -> term\<close> \<^vs>\<open>-0.2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.mk_conj : term * term -> term\<close> \<^vs>\<open>-0.2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.dest_conj : term -> term list\<close> \<^vs>\<open>-0.2cm\<close>
|
||||
\<^enum> \<^ML>\<open>HOLogic.conjuncts : term -> term list\<close> \<^vs>\<open>-0.2cm\<close>
|
||||
\<^enum> ...
|
||||
\<close>
|
||||
|
||||
|
|
@ -2312,7 +2312,6 @@ for Unicode Character Denotations as well as many local hints for improvements.\
|
|||
|
||||
section*[bib::bibliography]\<open>Bibliography\<close>
|
||||
|
||||
|
||||
close_monitor*[this]
|
||||
check_doc_global
|
||||
|
||||
|
|
|
|||
|
|
@ -435,7 +435,8 @@ val parse_define_shortcut = Parse.binding
|
|||
|
||||
fun define_macro (X,NONE) = (uncurry(uncurry(uncurry DOF_lib.define_macro)))(X,K(K()))
|
||||
|define_macro (X,SOME(src:Input.source)) =
|
||||
let val check_code = K(K())
|
||||
let val check_code = K(K()) (* hack *)
|
||||
val _ = warning "Checker code support Not Yet Implemented - use ML"
|
||||
in (uncurry(uncurry(uncurry DOF_lib.define_macro)))(X,check_code)
|
||||
end;
|
||||
|
||||
|
|
@ -444,6 +445,16 @@ val _ = Outer_Syntax.command \<^command_keyword>\<open>define_macro*\<close> "d
|
|||
|
||||
\<close>
|
||||
|
||||
ML\<open>ML_Context.expression\<close>
|
||||
(*
|
||||
fun setup source =
|
||||
ML_Context.expression (Input.pos_of source)
|
||||
(ML_Lex.read "Theory.setup (" @ ML_Lex.read_source source @ ML_Lex.read ")")
|
||||
|> Context.theory_map;
|
||||
setup\<open>\<close>
|
||||
|
||||
*)
|
||||
|
||||
|
||||
section\<open>Tables\<close>
|
||||
(* TODO ! ! ! *)
|
||||
|
|
|
|||
|
|
@ -469,7 +469,7 @@ setup\<open> let val cidS = ["scholarly_paper.introduction","scholarly_paper.tec
|
|||
true)
|
||||
in DOF_core.update_class_invariant "scholarly_paper.article" body end\<close>
|
||||
|
||||
|
||||
ML\<open> \<close>
|
||||
|
||||
section\<open>Miscelleous\<close>
|
||||
|
||||
|
|
@ -486,8 +486,7 @@ local
|
|||
|
||||
val scan_cm = Scan.ahead (Basic_Symbol_Pos.$$$ "c" |-- Basic_Symbol_Pos.$$$ "m" ) ;
|
||||
val scan_pt = Scan.ahead (Basic_Symbol_Pos.$$$ "p" |-- Basic_Symbol_Pos.$$$ "t" ) ;
|
||||
|
||||
val scan_blank = Scan.repeat (Basic_Symbol_Pos.$$$ " "
|
||||
val scan_blank = Scan.repeat ( Basic_Symbol_Pos.$$$ " "
|
||||
|| Basic_Symbol_Pos.$$$ "\t"
|
||||
|| Basic_Symbol_Pos.$$$ "\n");
|
||||
|
||||
|
|
@ -505,25 +504,24 @@ fun check_latex_measure _ src =
|
|||
let val _ = ((Scan.catch scan_latex_measure (Symbol_Pos.explode(Input.source_content src)))
|
||||
handle Fail _ => error ("syntax error in LaTeX measure") )
|
||||
in () end
|
||||
end
|
||||
|
||||
\<close>
|
||||
|
||||
ML\<open> (* test *) check_latex_measure @{context} (Input.string "-3.14 cm") \<close>
|
||||
|
||||
define_macro* hs \<rightleftharpoons> \<open>\hspace{\<close> _ \<open>}\<close> (check_latex_measure)
|
||||
define_macro* vs \<rightleftharpoons> \<open>\vspace{\<close> _ \<open>}\<close> (check_latex_measure)
|
||||
end\<close>
|
||||
|
||||
|
||||
|
||||
setup\<open> DOF_lib.define_macro \<^binding>\<open>vs2\<close> "\\vspace{" "}" (check_latex_measure) \<close>
|
||||
setup\<open> DOF_lib.define_macro \<^binding>\<open>vs\<close> "\\vspace{" "}" (check_latex_measure) \<close>
|
||||
setup\<open> DOF_lib.define_macro \<^binding>\<open>hs\<close> "\\hspace{" "}" (check_latex_measure) \<close>
|
||||
|
||||
text\<open> \<^vs2>\<open>-3.14cm\<close>\<close>
|
||||
(*<*)
|
||||
|
||||
text\<open>Tests: \<^vs>\<open>-0.14cm\<close>\<close>
|
||||
ML\<open> check_latex_measure @{context} (Input.string "-3.14 cm") \<close>
|
||||
define_macro* vs2 \<rightleftharpoons> \<open>\vspace{\<close> _ \<open>}\<close> (check_latex_measure) (* checkers NYI on Isar-level *)
|
||||
define_macro* hs2 \<rightleftharpoons> \<open>\hspace{\<close> _ \<open>}\<close> (* works fine without checker.*)
|
||||
|
||||
(*>*)
|
||||
|
||||
define_shortcut* clearpage \<rightleftharpoons> \<open>\clearpage{}\<close>
|
||||
|
||||
|
||||
|
||||
|
||||
end
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue