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:43:22 +01:00
parent 005922ffda
commit 4c5fc4bc53
1 changed files with 4 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/DOF/Isa_COL.thy
View File

@ -427,23 +427,21 @@ end
ML\<open>
val parse_literal = Parse.alt_string || Parse.cartouche
val parse_define_shortcut = (Parse.binding
-- ((\<^keyword>\<open>\<rightleftharpoons>\<close> || \<^keyword>\<open>==\<close>) |-- parse_literal))
val parse_define_shortcut = Parse.binding
-- ((\<^keyword>\<open>\<rightleftharpoons>\<close> || \<^keyword>\<open>==\<close>) |-- parse_literal)
--|Parse.underscore
-- parse_literal
-- (Scan.option (\<^keyword>\<open>(\<close> |-- Parse.ML_source --|\<^keyword>\<open>)\<close>))
fun define_macro (X,NONE) = (uncurry(uncurry(uncurry DOF_lib.define_macro)))(X,K(K()))
|define_macro (X,SOME(src:Input.source)) =
let val _ = ()
in
(uncurry(uncurry(uncurry DOF_lib.define_macro)))(X,K(K()))
let val check_code = K(K())
in (uncurry(uncurry(uncurry DOF_lib.define_macro)))(X,check_code)
end;
val _ = Outer_Syntax.command \<^command_keyword>\<open>define_macro*\<close> "define LaTeX shortcut"
(Scan.repeat1 parse_define_shortcut >> (Toplevel.theory o (fold define_macro)));
Parse.underscore;
\<close>