Merge branch 'main' into isabelle_nightly

Isabelle_DOF-Example-I/ROOT

@@ -1,5 +1,7 @@
+chapter AFP
+
 session "Isabelle_DOF-Example-I" (AFP) = "Isabelle_DOF" + 
-  options [document = pdf, document_output = "output", document_build = dof]
+  options [document = pdf, document_output = "output", document_build = dof, timeout = 300]
   theories
     IsaDofApplications
   document_files

Isabelle_DOF-Example-I/document/lstisadof-manual.sty

@@ -90,9 +90,7 @@
      ,enhanced jigsaw
      ,borderline west={2pt}{0pt}{isar!60!black}
      ,sharp corners
-     ,before skip balanced=0.5\baselineskip plus 2pt
-     % ,before skip=10pt
-     % ,after skip=10pt
+     %,before skip balanced=0.5\baselineskip plus 2pt % works only with Tex Live 2020 and later
      ,enlarge top by=0mm
      ,enhanced
      ,overlay={\node[draw,fill=isar!60!black,xshift=0pt,anchor=north

Isabelle_DOF-Example-II/ROOT

@@ -1,5 +1,7 @@
-session "Isabelle_DOF-Example-II" = "Isabelle_DOF" +
-  options [document = pdf, document_output = "output", document_build = dof]
+chapter AFP 
+
+session "Isabelle_DOF-Example-II" (AFP) = "Isabelle_DOF" +
+  options [document = pdf, document_output = "output", document_build = dof, timeout = 300]
   theories
     "paper"
   document_files

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-Ontologies/document/lstisadof-manual.sty

@@ -90,9 +90,7 @@
      ,enhanced jigsaw
      ,borderline west={2pt}{0pt}{isar!60!black}
      ,sharp corners
-     ,before skip balanced=0.5\baselineskip plus 2pt
-     % ,before skip=10pt
-     % ,after skip=10pt
+     %,before skip balanced=0.5\baselineskip plus 2pt % works only with Tex Live 2020 and later
      ,enlarge top by=0mm
      ,enhanced
      ,overlay={\node[draw,fill=isar!60!black,xshift=0pt,anchor=north

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/ROOT

@@ -1,5 +1,7 @@
+chapter AFP
+
 session "Isabelle_DOF" (AFP) = "Functional-Automata" + 
-  options [document = pdf, document_output = "output", document_build = dof]
+  options [document = pdf, document_output = "output", document_build = dof, timeout = 300]
   sessions
     "Regular-Sets"
   directories 
@@ -31,7 +33,6 @@ session "Isabelle_DOF" (AFP) = "Functional-Automata" +
     "lstisadof-manual.sty" 
     "figures/cicm2018-combined.png"
     "figures/document-hierarchy.pdf"
-    "figures/document-hierarchy.svg"
     "figures/Dogfood-figures.png"
     "figures/Dogfood-II-bgnd1.png"
     "figures/Dogfood-III-bgnd-text_section.png"
@@ -39,7 +40,6 @@ session "Isabelle_DOF" (AFP) = "Functional-Automata" +
     "figures/Dogfood-V-attribute.png"
     "figures/Dogfood-VI-linkappl.png"
     "figures/isabelle-architecture.pdf"
-    "figures/isabelle-architecture.svg"
     "figures/Isabelle_DOF-logo.pdf"
     "figures/header_CSP_pdf.png"
     "figures/header_CSP_source.png"

Isabelle_DOF/document/lstisadof-manual.sty

@@ -90,9 +90,7 @@
      ,enhanced jigsaw
      ,borderline west={2pt}{0pt}{isar!60!black}
      ,sharp corners
-     ,before skip balanced=0.5\baselineskip plus 2pt
-     % ,before skip=10pt
-     % ,after skip=10pt
+     %,before skip balanced=0.5\baselineskip plus 2pt % works only with Tex Live 2020 and later
      ,enlarge top by=0mm
      ,enhanced
      ,overlay={\node[draw,fill=isar!60!black,xshift=0pt,anchor=north

Isabelle_DOF/thys/Isa_DOF.thy

@@ -3008,8 +3008,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