From 4c5fc4bc534cd531b28709b850c4dfd0c9e0d220 Mon Sep 17 00:00:00 2001
From: Burkhart Wolff <wolff@lri.fr>
Date: Wed, 23 Dec 2020 09:43:22 +0100
Subject: [PATCH] built in syntactic checks for trimming macros

---
 src/DOF/Isa_COL.thy | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy
index ad0ef05..58b7963 100755
--- a/src/DOF/Isa_COL.thy
+++ b/src/DOF/Isa_COL.thy
@@ -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>