Merge.

Isabelle_DOF-Examples-Extra/beamerx/presentation/presentation.thy

@@ -19,6 +19,18 @@ text\<open>
 \end{frame}
 \<close>
 
+frame*[test_frame
+    , frametitle = \<open>\<open>\<open>Example Slide\<^sub>t\<^sub>e\<^sub>s\<^sub>t\<close> @{thm "HOL.refl"}\<close>\<close>
+    , framesubtitle = "''Subtitle''"]
+\<open>This is an example!
+ \<^item> The term \<^term>\<open>refl\<close> is...
+ \<^item> and the term encoding the title of this frame is \<^term_>\<open>frametitle @{frame \<open>test_frame\<close>}\<close>\<close>
+
+frame*[test_frame2
+    , frametitle = "''Example Slide''"
+    , framesubtitle = \<open>\<open>\<open>Subtitle\<^sub>t\<^sub>e\<^sub>s\<^sub>t:\<close> the value of \<^term>\<open>(3::int) + 3\<close> is @{value "(3::int) + 3"}\<close>\<close>]
+\<open>Test frame env \<^term>\<open>refl\<close>\<close>
+
 (*<*)
 end 
 (*>*)

Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy

@@ -206,11 +206,10 @@ ML\<open>
 map fst (Name_Space.dest_table (DOF_core.get_onto_classes \<^context>));
 
 let  val class_ids_so_far = ["Conceptual.A", "Conceptual.B", "Conceptual.C", "Conceptual.D", 
-                             "Conceptual.E", "Conceptual.F", "Conceptual.G", "Conceptual.M", 
-                             "Isa_COL.float", "Isa_COL.figure", "Isa_COL.chapter", "Isa_COL.listing", 
-                             "Isa_COL.section", 
-                             "Isa_COL.paragraph", "Isa_COL.subsection", 
-                             "Isa_COL.text_element", "Isa_COL.subsubsection"]
+                             "Conceptual.E", "Conceptual.F", "Conceptual.G", "Conceptual.M",
+                             "Isa_COL.float", "Isa_COL.frame", "Isa_COL.figure", "Isa_COL.chapter",
+                             "Isa_COL.listing", "Isa_COL.section", "Isa_COL.paragraph",
+                             "Isa_COL.subsection", "Isa_COL.text_element", "Isa_COL.subsubsection"]
      val docclass_tab = map fst (Name_Space.dest_table (DOF_core.get_onto_classes \<^context>));
 in @{assert} (class_ids_so_far = docclass_tab) end\<close>
 

Isabelle_DOF/thys/Isa_COL.thy

@@ -26,7 +26,7 @@ theory Isa_COL
   keywords "title*"        "subtitle*"      
            "chapter*"      "section*"    "paragraph*"
            "subsection*"   "subsubsection*" 
-           "figure*"       "listing*"   :: document_body 
+           "figure*"       "listing*"    "frame*" :: document_body
 
 begin
 
@@ -269,15 +269,24 @@ val mt_fig_content = {relative_width  = 100,
                       relative_height = 100,    
                       caption         = Input.empty }: fig_content
 
-fun upd_relative_width key {relative_width,relative_height,caption } : fig_content = 
-            {relative_width = key,relative_height = relative_height,caption = caption}: fig_content
+fun make_fig_content (relative_width, relative_height, caption) =
+   {relative_width = relative_width, relative_height = relative_height, caption = caption}
 
-fun upd_relative_height key  {relative_width,relative_height,caption } : fig_content = 
-            {relative_width = relative_width,relative_height = key,caption = caption}: fig_content
+fun upd_fig_content f =
+  fn {relative_width, relative_height, caption} =>
+    make_fig_content (f (relative_width, relative_height, caption))
 
-fun upd_caption key {relative_width,relative_height,caption} : fig_content = 
-            {relative_width = relative_width,relative_height = relative_height,caption= key}: fig_content
+fun upd_relative_width f =
+  upd_fig_content (fn (relative_width, relative_height, caption) =>
+    (f relative_width, relative_height, caption))
 
+fun upd_relative_height f =
+  upd_fig_content (fn (relative_width, relative_height, caption) =>
+    (relative_width, f relative_height, caption))
+
+fun upd_caption f =
+  upd_fig_content (fn (relative_width, relative_height, caption) =>
+    (relative_width, relative_height, f caption))
 
 val widthN     = "width"
 val heightN    = "height" 
@@ -288,11 +297,11 @@ fun fig_content_modes (ctxt, toks) =
                       (Args.parens 
                          (Parse.list1
                            (   (Args.$$$ widthN |-- Args.$$$ "=" -- Parse.int
-                                >> (fn (_, k) => upd_relative_width k))   
+                                >> (fn (_, k) => upd_relative_width (K k)))
                             || (Args.$$$ heightN |-- Args.$$$ "=" -- Parse.int
-                                >> (fn (_, k) => upd_relative_height k))    
+                                >> (fn (_, k) => upd_relative_height (K k)))
                             || (Args.$$$ captionN |-- Args.$$$ "=" -- Parse.document_source
-                                >> (fn (_, k) => upd_caption k))    
+                                >> (fn (_, k) => upd_caption (K k)))
                       ))) [K mt_fig_content]) 
                       : (fig_content -> fig_content) list parser)
                       >> (foldl1 (op #>)))
@@ -372,9 +381,9 @@ fun convert_meta_args ctxt (X, (((str,_),value) :: R)) =
                           handle TERM _ =>  error "Illegal int format."
      in
          (case YXML.content_of str of 
-             "relative_width" =>  upd_relative_width (conv_int value)
+             "relative_width" =>  upd_relative_width (K (conv_int value))
                                   o  convert_meta_args ctxt (X, R)
-          |  "relative_height" => upd_relative_height (conv_int value) 
+          |  "relative_height" => upd_relative_height (K (conv_int value))
                                   o  convert_meta_args ctxt (X, R )
           |  "file_src"        => convert_meta_args ctxt (X, R)
           |  s => error("!undefined attribute:"^s))
@@ -404,11 +413,11 @@ fun float_command (name, pos) descr cid  =
                                |> Latex.string)
       fun parse_and_tex (margs as (((oid, _),_), _), cap_src) ctxt =
         (convert_src_from_margs ctxt margs)
-        |> pair (upd_caption Input.empty #> convert_meta_args ctxt margs)
+        |> pair (upd_caption (K Input.empty) #> convert_meta_args ctxt margs)
         |> fig_content ctxt 
         |> generate_fig_ltx_ctxt ctxt cap_src oid
         |> (Latex.environment ("figure") )
-  in  Monitor_Command_Parser.float_command (name, pos) descr create_instance parse_and_tex
+  in  Monitor_Command_Parser.onto_macro_cmd_command (name, pos) descr create_instance parse_and_tex
   end
 
 fun listing_command (name, pos) descr cid  =
@@ -421,7 +430,7 @@ fun listing_command (name, pos) descr cid  =
                {define = true} oid pos (set_default_class cid_pos) doc_attrs
       fun parse_and_tex (margs as (((_, pos),_), _), _) _ =
         ISA_core.err ("Not yet implemented.\n Please use text*[oid::listing]\<open>\<close> instead.") pos
-  in  Monitor_Command_Parser.float_command (name, pos) descr create_instance parse_and_tex
+  in  Monitor_Command_Parser.onto_macro_cmd_command (name, pos) descr create_instance parse_and_tex
   end
   
 
@@ -715,5 +724,75 @@ text\<open> @{table_inline  [display] (cell_placing = center,cell_height =\<open
 
 (*>*)
 
+text\<open>beamer frame environment\<close>
+(* Under development *)
+
+doc_class frame =
+  frametitle :: string
+  framesubtitle :: string
+
+ML\<open>
+type frame = {frametitle: Input.source, framesubtitle: Input.source}
+
+val empty_frame = {frametitle = Input.empty, framesubtitle = Input.empty}: frame
+
+fun make_frame (frametitle, framesubtitle) =
+  {frametitle = frametitle, framesubtitle = framesubtitle}
+
+fun upd_frame f =
+  fn {frametitle, framesubtitle} => make_frame (f (frametitle, framesubtitle))
+
+fun upd_frametitle f =
+  upd_frame (fn (frametitle, framesubtitle) => (f frametitle, framesubtitle))
+
+fun upd_framesubtitle f =
+  upd_frame (fn (frametitle, framesubtitle) => (frametitle, f framesubtitle))
+
+val unenclose_end = unenclose
+val unenclose_string = unenclose o unenclose o unenclose_end
+
+fun read_string s =
+  let val symbols = unenclose_end s |> Symbol_Pos.explode0
+  in if hd symbols |> fst |> equal Symbol.open_
+     then Token.read_cartouche symbols |> Token.input_of
+     else unenclose_string s |> Syntax.read_input
+  end
+
+fun convert_meta_args ctxt (X, (((str,_),value) :: R)) =
+  (case YXML.content_of str of
+             "frametitle" =>  upd_frametitle (K(YXML.content_of value |> read_string))
+                                  o  convert_meta_args ctxt (X, R)
+          |  "framesubtitle" => upd_framesubtitle (K(YXML.content_of value |> read_string))
+                                  o  convert_meta_args ctxt (X, R )
+          |  s => error("!undefined attribute:"^s))
+  | convert_meta_args _ (_,[]) = I
+
+fun frame_command (name, pos) descr cid  =
+  let fun set_default_class NONE = SOME(cid,pos)
+         |set_default_class (SOME X) = SOME X
+      fun create_instance  ((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t)  =
+                Value_Command.Docitem_Parser.create_and_check_docitem
+               {is_monitor = false}
+               {is_inline = true}
+               {define = true} oid pos (set_default_class cid_pos) doc_attrs
+      fun generate_src_ltx_ctxt ctxt src cfg_trans =
+        let val {frametitle, framesubtitle} = cfg_trans empty_frame
+        in Latex.string "{"
+           @ Document_Output.output_document ctxt {markdown = false} frametitle
+           @ Latex.string "}"
+           @ Latex.string "{"
+           @ (Document_Output.output_document ctxt {markdown = false} framesubtitle)
+           @ Latex.string "}"
+           @ Document_Output.output_document ctxt {markdown = true} src
+       end
+      fun parse_and_tex (margs, src) ctxt =
+        convert_meta_args ctxt margs
+        |> generate_src_ltx_ctxt ctxt src
+        |> (Latex.environment ("frame") )
+  in  Monitor_Command_Parser.onto_macro_cmd_command (name, pos) descr create_instance parse_and_tex
+  end
+
+val _ = frame_command \<^command_keyword>\<open>frame*\<close> "frame environment" "Isa_COL.frame" ;
+\<close>
 
 end

Isabelle_DOF/thys/Isa_DOF.thy

@@ -2199,18 +2199,22 @@ fun document_output_reports name {markdown, body} sem_attrs transform_attr meta_
 
 fun document_command (name, pos) descr mark cmd sem_attrs transform_attr =
   Outer_Syntax.command (name, pos) descr
-    (ODL_Meta_Args_Parser.attributes -- Parse.document_source >> (fn (meta_args, text) =>
+  (ODL_Meta_Args_Parser.attributes -- Parse.document_source >> (fn (meta_args, text) =>
       Toplevel.theory' (fn _ => cmd meta_args)
           (SOME (Toplevel.presentation_context #> document_output_reports name mark sem_attrs transform_attr meta_args text)))); 
 
-fun float_command (name, pos) descr
-                   cmd  output_figure = 
+fun onto_macro_cmd_output_reports output_figure (meta_args, text) ctxt =
+ let
+   val _ = Context_Position.reports ctxt (Document_Output.document_reports text);
+ in output_figure (meta_args, text) ctxt end
+
+fun onto_macro_cmd_command (name, pos) descr cmd output_cmd = 
   Outer_Syntax.command (name, pos) descr 
   (ODL_Meta_Args_Parser.attributes -- Parse.document_source >>  
      (fn (meta_args, text) =>
           Toplevel.theory' (fn _ => cmd meta_args)
              (SOME (Toplevel.presentation_context
-              #> output_figure (meta_args, text)
+              #> onto_macro_cmd_output_reports output_cmd  (meta_args, text)
               ))))