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

built in syntactic checks for trimming macros

This commit is contained in:
Burkhart Wolff 2020-12-23 09:41:26 +01:00
parent 6899c4059e
commit 005922ffda
2 changed files with 37 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy
View File

@ -33,7 +33,7 @@ define_shortcut* TeXLive \<rightleftharpoons> \<open>\TeXLive\<close>
text\<open>Note that these setups assume that the associated \<^LaTeX> macros
are defined, \<^eg>, in the document prelude. \<close>
define_macro* index \<rightleftharpoons> \<open>\index{\<close> _ \<open>}\<close>
define_macro* index \<rightleftharpoons> \<open>\index{\<close> _ \<open>}\<close>
define_macro* bindex \<rightleftharpoons> \<open>\bindex{\<close> _ \<open>}\<close>

42
src/ontologies/scholarly_paper/scholarly_paper.thy
View File

@ -479,16 +479,46 @@ define_shortcut* eg \<rightleftharpoons> \<open>\eg\<close> (* Latin: „exemp
ie \<rightleftharpoons> \<open>\ie\<close> (* Latin: „id est“ meaning „that is to say“. *)
etc \<rightleftharpoons> \<open>\etc\<close> (* Latin : „et cetera“ meaning „et cetera“ *)
subsection\<open>Layout Trimming Commands\<close>
subsection\<open>Layout Trimming Commands (with syntactic checks)\<close>
define_macro* hs \<rightleftharpoons> \<open>\hspace{\<close> _ \<open>}\<close>
define_macro* vs \<rightleftharpoons> \<open>\vspace{\<close> _ \<open>}\<close>
ML\<open>
local
(* setup\<open> DOF_lib.define_macro \<^binding>\<open>hs\<close> "\\hspace{" "}" (K(K())) \<close> *)
ML\<open> Parse.real \<close>
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" ) ;
setup\<open> DOF_lib.define_macro \<^binding>\<open>vs2\<close> "\\vspace{" "}" (fn ctxt => fn src => ()) \<close>
val scan_blank = Scan.repeat (Basic_Symbol_Pos.$$$ " "
|| Basic_Symbol_Pos.$$$ "\t"
|| Basic_Symbol_Pos.$$$ "\n");
val scan_latex_measure = (scan_blank
|-- Scan.option (Basic_Symbol_Pos.$$$ "-")
|-- Symbol_Pos.scan_nat
|-- (Scan.option ((Basic_Symbol_Pos.$$$ ".") |-- Symbol_Pos.scan_nat))
|-- scan_blank
|-- (scan_cm || scan_pt)
|-- scan_blank
);
in
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)
setup\<open> DOF_lib.define_macro \<^binding>\<open>vs2\<close> "\\vspace{" "}" (check_latex_measure) \<close>
text\<open> \<^vs2>\<open>-3.14cm\<close>\<close>
define_shortcut* clearpage \<rightleftharpoons> \<open>\clearpage{}\<close>