diff --git a/Isabelle_DOF-Examples-Extra/beamerx/presentation/ROOT b/Isabelle_DOF-Examples-Extra/beamerx/presentation/ROOT index ebe69c1..4478623 100644 --- a/Isabelle_DOF-Examples-Extra/beamerx/presentation/ROOT +++ b/Isabelle_DOF-Examples-Extra/beamerx/presentation/ROOT @@ -6,3 +6,4 @@ session "presentation-example" (AFP) = "Isabelle_DOF-Ontologies" + "presentation" document_files "preamble.tex" + "figures/A.png" diff --git a/Isabelle_DOF-Examples-Extra/beamerx/presentation/document/figures/A.png b/Isabelle_DOF-Examples-Extra/beamerx/presentation/document/figures/A.png new file mode 100644 index 0000000..0221da4 Binary files /dev/null and b/Isabelle_DOF-Examples-Extra/beamerx/presentation/document/figures/A.png differ diff --git a/Isabelle_DOF-Examples-Extra/beamerx/presentation/presentation.thy b/Isabelle_DOF-Examples-Extra/beamerx/presentation/presentation.thy index 3b7c536..0c11741 100644 --- a/Isabelle_DOF-Examples-Extra/beamerx/presentation/presentation.thy +++ b/Isabelle_DOF-Examples-Extra/beamerx/presentation/presentation.thy @@ -19,8 +19,9 @@ text\ \end{frame} \ + frame*[test_frame - , frametitle = \\\Example Slide\<^sub>t\<^sub>e\<^sub>s\<^sub>t\ @{thm "HOL.refl"}\\ + , frametitle = \\\Example Slide\<^sub>t\<^sub>e\<^sub>s\<^sub>t\ with items @{thm "HOL.refl"}\\ , framesubtitle = "''Subtitle''"] \This is an example! \<^item> The term \<^term>\refl\ is... @@ -31,6 +32,38 @@ frame*[test_frame2 , 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\\ +frame*[test_frame3, frametitle = "''A slide with a Figure''"] +\A figure +@{figure_content (width=45, caption=\\Figure\<^sub>t\<^sub>e\<^sub>s\<^sub>t\ is not the \<^term>\refl\ theorem (@{thm "refl"}).\) + "figures/A.png"}\ + +frame*[test_frame4 + , options = "''allowframebreaks''" + , frametitle = "''Example Slide with frame break''" + , framesubtitle = \\\Subtitle\<^sub>t\<^sub>e\<^sub>s\<^sub>t:\ the value of \<^term>\(3::int) + 3\ is @{value "(3::int) + 3"}\\] +\ + \<^item> The term \<^term>\refl\ is... + \<^item> and the term encoding the title of this frame is \<^term_>\frametitle @{frame \test_frame4\}\ + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... +\ + (*<*) end (*>*) diff --git a/Isabelle_DOF/thys/Isa_COL.thy b/Isabelle_DOF/thys/Isa_COL.thy index 2db41dc..6d4aed8 100644 --- a/Isabelle_DOF/thys/Isa_COL.thy +++ b/Isabelle_DOF/thys/Isa_COL.thy @@ -331,25 +331,34 @@ fun generate_caption ctxt caption = in drop_latex_macros cap_txt end + +fun process_args cfg_trans = + let val {relative_width,relative_height,caption} = cfg_trans mt_fig_content + val _ = if relative_width < 0 orelse relative_height <0 + then error("negative parameter.") + else () + val wdth_val_s = Real.toString((Real.fromInt relative_width) + / (Real.fromInt 100))^"\\textwidth" + val ht_s= if relative_height = 100 + then "" + else "height=" + ^ Real.toString((Real.fromInt relative_height) + / (Real.fromInt 100)) + ^ "\\textheight" + in (wdth_val_s, ht_s, caption) end + fun fig_content ctxt (cfg_trans,file:Input.source) = - let val {relative_width,relative_height,caption} = cfg_trans mt_fig_content - val _ = if relative_width < 0 orelse relative_height <0 then error("negative parameter.") - else () - val wdth_val_s = Real.toString((Real.fromInt relative_width) - / (Real.fromInt 100))^"\\textwidth" - val ht_s= if relative_height = 100 then "" - else "height="^Real.toString((Real.fromInt relative_height) - / (Real.fromInt 100)) ^"\\textheight" - val arg_single = enclose "[" "]" (commas ["keepaspectratio","width="^wdth_val_s,ht_s]) - val arg = enclose "[" "]" (commas ["keepaspectratio","width=\\textwidth",ht_s]) - val _ = Resources.check_file ctxt (SOME (get_document_dir ctxt)) file - (* ToDo: must be declared source of type png or jpeg or pdf, ... *) + let val (wdth_val_s, ht_s, caption) = process_args cfg_trans + val arg_single = enclose "[" "]" (commas ["keepaspectratio","width="^wdth_val_s,ht_s]) + val arg = enclose "[" "]" (commas ["keepaspectratio","width=\\textwidth",ht_s]) + val _ = Resources.check_file ctxt (SOME (get_document_dir ctxt)) file + (* ToDo: must be declared source of type png or jpeg or pdf, ... *) - in if Input.string_of(caption) = "" then + in if Input.string_of(caption) = "" then file |> (Latex.string o Input.string_of) |> Latex.macro ("includegraphics"^arg_single) - else + else file |> (Latex.string o Input.string_of) |> (fn X => (Latex.string ("{"^wdth_val_s^"}")) @@ -358,7 +367,7 @@ fun fig_content ctxt (cfg_trans,file:Input.source) = @ (Latex.macro "caption" (generate_caption ctxt caption))) |> (Latex.environment ("subcaptionblock") ) (* BUG: newline at the end of subcaptionlbock, making side-by-side a figure-below-figure setup *) - end + end fun fig_content_antiquotation name scan = (Document_Output.antiquotation_raw_embedded name @@ -366,8 +375,27 @@ fun fig_content_antiquotation name scan = (fig_content : Proof.context -> (fig_content -> fig_content) * Input.source -> Latex.text)); +fun figure_content ctxt (cfg_trans,file:Input.source) = + let val (wdth_val_s, ht_s, caption) = process_args cfg_trans + val args = ["keepaspectratio","width=" ^ wdth_val_s, ht_s] + |> commas + |> enclose "[" "]" + in file + |> (Latex.string o Input.string_of) + |> Latex.macro ("includegraphics" ^ args) + |> (fn X => X @ Latex.macro "caption" (generate_caption ctxt caption)) + |> Latex.environment ("figure") + end + +fun figure_antiquotation name scan = + (Document_Output.antiquotation_raw_embedded name + (scan : ((fig_content -> fig_content) * Input.source) context_parser) + (figure_content : Proof.context -> (fig_content -> fig_content) * Input.source -> Latex.text)); + val _ = Theory.setup ( fig_content_antiquotation \<^binding>\fig_content\ + (fig_content_modes -- Scan.lift(Parse.path_input)) + #> figure_antiquotation \<^binding>\figure_content\ (fig_content_modes -- Scan.lift(Parse.path_input))) \ @@ -728,25 +756,33 @@ text\beamer frame environment\ (* Under development *) doc_class frame = + options :: string frametitle :: string framesubtitle :: string ML\ -type frame = {frametitle: Input.source, framesubtitle: Input.source} +type frame = {options: Input.source + , frametitle: Input.source + , framesubtitle: Input.source} -val empty_frame = {frametitle = Input.empty, framesubtitle = Input.empty}: frame +val empty_frame = {options = Input.empty + , frametitle = Input.empty + , framesubtitle = Input.empty}: frame -fun make_frame (frametitle, framesubtitle) = - {frametitle = frametitle, framesubtitle = framesubtitle} +fun make_frame (options, frametitle, framesubtitle) = + {options = options, frametitle = frametitle, framesubtitle = framesubtitle} fun upd_frame f = - fn {frametitle, framesubtitle} => make_frame (f (frametitle, framesubtitle)) + fn {options, frametitle, framesubtitle} => make_frame (f (options, frametitle, framesubtitle)) + +fun upd_options f = + upd_frame (fn (options, frametitle, framesubtitle) => (f options, frametitle, framesubtitle)) fun upd_frametitle f = - upd_frame (fn (frametitle, framesubtitle) => (f frametitle, framesubtitle)) + upd_frame (fn (options, frametitle, framesubtitle) => (options, f frametitle, framesubtitle)) fun upd_framesubtitle f = - upd_frame (fn (frametitle, framesubtitle) => (frametitle, f framesubtitle)) + upd_frame (fn (options, frametitle, framesubtitle) => (options, frametitle, f framesubtitle)) val unenclose_end = unenclose val unenclose_string = unenclose o unenclose o unenclose_end @@ -759,12 +795,14 @@ fun read_string s = 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)) + (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) + | "options" => upd_options (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 = @@ -775,21 +813,31 @@ fun frame_command (name, pos) descr cid = {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 "{" + fun titles_src ctxt frametitle framesubtitle src = 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 + fun generate_src_ltx_ctxt ctxt src cfg_trans = + let val {options, frametitle, framesubtitle} = cfg_trans empty_frame + in + let val options_str = Input.string_of options + in if options_str = "" + then titles_src ctxt frametitle framesubtitle src + else (options_str + |> enclose "[" "]" + |> Latex.string) + @ titles_src ctxt frametitle framesubtitle src + end 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 + |> Latex.environment ("frame") + |> Latex.environment ("isamarkuptext") + 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" ; diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy index 914d0aa..7c4f238 100644 --- a/Isabelle_DOF/thys/Isa_DOF.thy +++ b/Isabelle_DOF/thys/Isa_DOF.thy @@ -2206,10 +2206,10 @@ fun document_command (name, pos) descr mark cmd sem_attrs transform_attr = #> document_output_reports name mark sem_attrs transform_attr meta_args text #> SOME): Toplevel.state -> Latex.text option)) ); -fun onto_macro_cmd_output_reports output_figure (meta_args, text) ctxt = +fun onto_macro_cmd_output_reports output_cmd (meta_args, text) ctxt = let val _ = Context_Position.reports ctxt (Document_Output.document_reports text); - in output_figure (meta_args, text) ctxt end + in output_cmd (meta_args, text) ctxt end fun onto_macro_cmd_command (name, pos) descr cmd output_cmd = Outer_Syntax.command (name, pos) descr