From 4d89250606134cb8e628526ceaef2faca0ef1a9d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= <nicolasmeric@posteo.net>
Date: Tue, 16 May 2023 12:27:19 +0200
Subject: [PATCH] Restrict RegExpInterface notations to onto class definition

---
 Isabelle_DOF-Unit-Tests/Attributes.thy | 11 +++++++++++
 Isabelle_DOF/thys/Isa_DOF.thy          |  4 ++++
 Isabelle_DOF/thys/RegExpInterface.thy  | 16 +++++++++++++++-
 3 files changed, 30 insertions(+), 1 deletion(-)

diff --git a/Isabelle_DOF-Unit-Tests/Attributes.thy b/Isabelle_DOF-Unit-Tests/Attributes.thy
index cac9eb58..2dab8f10 100644
--- a/Isabelle_DOF-Unit-Tests/Attributes.thy
+++ b/Isabelle_DOF-Unit-Tests/Attributes.thy
@@ -202,7 +202,18 @@ section\<open>A Complex Evaluation involving Automatas\<close>
 
 text\<open>Test trace\_attribute term antiquotation:\<close>
 
+notation Star  ("\<lbrace>(_)\<rbrace>\<^sup>*" [0]100)
+notation Plus  (infixr "||" 55)
+notation Times (infixr "~~" 60)
+notation Atom  ("\<lfloor>_\<rfloor>" 65)
+
 definition example_expression where "example_expression \<equiv> \<lbrace>\<lfloor>''Conceptual.A''\<rfloor> || \<lfloor>''Conceptual.F''\<rfloor>\<rbrace>\<^sup>*"
+
+no_notation Star  ("\<lbrace>(_)\<rbrace>\<^sup>*" [0]100)
+no_notation Plus  (infixr "||" 55)
+no_notation Times (infixr "~~" 60)
+no_notation Atom  ("\<lfloor>_\<rfloor>" 65)
+
 value* \<open> DA.accepts (na2da (rexp2na example_expression)) (map fst @{trace-attribute \<open>aaa\<close>}) \<close>
 
 definition word_test  :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> bool" (infix "is-in" 60)
diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy
index df19e11f..3b62c5d8 100644
--- a/Isabelle_DOF/thys/Isa_DOF.thy
+++ b/Isabelle_DOF/thys/Isa_DOF.thy
@@ -3015,8 +3015,12 @@ fun add_doc_class_cmd overloaded (raw_params, binding)
                   , (Binding.empty_atts, Binding.name_of binding |> mk_eq_pair), [], [])
       fun add record_fields virtual =
         Record.add_record overloaded (params', binding) parent' record_fields
+        #> (Local_Theory.notation true Syntax.mode_default RegExpInterface_Notations.notations
+            |> Named_Target.theory_map)
         #> DOF_core.define_doc_class_global (params', binding) parent fieldsNterms' regexps 
                                             reject_Atoms invariants virtual
+        #> (Local_Theory.notation false Syntax.mode_default RegExpInterface_Notations.notations
+            |> Named_Target.theory_map)
     in thy    (* adding const symbol representing doc-class for Monitor-RegExps.*)
            |> Named_Target.theory_map (def_cmd args)
            |> (case parent' of
diff --git a/Isabelle_DOF/thys/RegExpInterface.thy b/Isabelle_DOF/thys/RegExpInterface.thy
index c28e96b3..660d1751 100644
--- a/Isabelle_DOF/thys/RegExpInterface.thy
+++ b/Isabelle_DOF/thys/RegExpInterface.thy
@@ -236,7 +236,21 @@ end; (* local *)
 end  (* struct *)
 \<close>
 
-no_notation Atom ("\<lfloor>_\<rfloor>")  
+no_notation Star  ("\<lbrace>(_)\<rbrace>\<^sup>*" [0]100)
+no_notation Plus  (infixr "||" 55)
+no_notation Times (infixr "~~" 60)
+no_notation Atom  ("\<lfloor>_\<rfloor>" 65)
+
+ML\<open>
+structure RegExpInterface_Notations =
+struct
+val Star = (\<^term>\<open>Regular_Exp.Star\<close>, Mixfix (Syntax.read_input "\<lbrace>(_)\<rbrace>\<^sup>*", [0], 100, Position.no_range))
+val Plus = (\<^term>\<open>Regular_Exp.Plus\<close>, Infixr (Syntax.read_input "||", 55, Position.no_range))
+val Times = (\<^term>\<open>Regular_Exp.Times\<close>, Infixr (Syntax.read_input "~~", 60, Position.no_range))
+val Atom = (\<^term>\<open>Regular_Exp.Atom\<close>, Mixfix (Syntax.read_input "\<lfloor>_\<rfloor>", [], 65, Position.no_range))
+val notations = [Star, Plus, Times, Atom]
+end
+\<close>
 
 end