diff --git a/Isabelle_DOF-Examples-Extra/beamerx/presentation/presentation.thy b/Isabelle_DOF-Examples-Extra/beamerx/presentation/presentation.thy index 1f70238..3b7c536 100644 --- a/Isabelle_DOF-Examples-Extra/beamerx/presentation/presentation.thy +++ b/Isabelle_DOF-Examples-Extra/beamerx/presentation/presentation.thy @@ -19,6 +19,18 @@ text\ \end{frame} \ +frame*[test_frame + , frametitle = \\\Example Slide\<^sub>t\<^sub>e\<^sub>s\<^sub>t\ @{thm "HOL.refl"}\\ + , framesubtitle = "''Subtitle''"] +\This is an example! + \<^item> The term \<^term>\refl\ is... + \<^item> and the term encoding the title of this frame is \<^term_>\frametitle @{frame \test_frame\}\\ + +frame*[test_frame2 + , frametitle = "''Example Slide''" + , framesubtitle = \\\Subtitle\<^sub>t\<^sub>e\<^sub>s\<^sub>t:\ the value of \<^term>\(3::int) + 3\ is @{value "(3::int) + 3"}\\] +\Test frame env \<^term>\refl\\ + (*<*) end (*>*) diff --git a/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy b/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy index f6d9172..75bb658 100644 --- a/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy +++ b/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy @@ -206,11 +206,10 @@ ML\ 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\ diff --git a/Isabelle_DOF/thys/Isa_COL.thy b/Isabelle_DOF/thys/Isa_COL.thy index 69f8012..2db41dc 100644 --- a/Isabelle_DOF/thys/Isa_COL.thy +++ b/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]\\ 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\ @{table_inline [display] (cell_placing = center,cell_height =\*) +text\beamer frame environment\ +(* Under development *) + +doc_class frame = + frametitle :: string + framesubtitle :: string + +ML\ +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>\frame*\ "frame environment" "Isa_COL.frame" ; +\ end diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy index f7d615b..ca61800 100644 --- a/Isabelle_DOF/thys/Isa_DOF.thy +++ b/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) ))))