Merge branch 'main' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF

Isabelle_DOF-Ontologies/document-templates/root-sn-article-UNSUPPORTED.tex

@@ -38,6 +38,10 @@
 } % more detailed digital TOC (aka bookmarks)
 \sloppy
 \allowdisplaybreaks[4]
+
+\usepackage{subcaption}
+\usepackage[size=footnotesize]{caption}
+
 \let\DOFauthor\relax
 \begin{document}
 \selectlanguage{USenglish}%

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)

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

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