Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

ported another Figure* in OutOfOrderPresntn to Isabelle2022
ci/woodpecker/push/build Pipeline was successful Details

This commit is contained in:
Burkhart Wolff 2022-11-09 06:06:30 +01:00
parent 2149db9efc
commit 830e1b440a
2 changed files with 5 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/DOF/Isa_COL.thy
View File

@ -623,7 +623,8 @@ declare[[tab_cell_placing="left",tab_cell_height="18.0cm"]]
section\<open>Tests\<close>
(*<*)
text\<open> @{fig_content [display] (scale = 80, width=80, caption=\<open>this is \<^term>\<open>\<sigma>\<^sub>i+2\<close> \<dots>\<close>) \<open>../ROOT\<close>}\<close>
text\<open> @{fig_content [display] (scale = 80, width=80, caption=\<open>this is \<^term>\<open>\<sigma>\<^sub>i+2\<close> \<dots>\<close>)
\<open>../../examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/isabelle-architecture.pdf\<close>}\<close>
text\<open> @{table_inline [display] (cell_placing = center,cell_height =\<open>12.0cm\<close>,
cell_height =\<open>13pt\<close>, cell_width = \<open>12.0cm\<close>,
cell_bgnd_color=black,cell_line_color=red,cell_line_width=\<open>12.0cm\<close>)

6
src/tests/OutOfOrderPresntn.thy
View File

@ -67,7 +67,7 @@ fun gen_enriched_document_command2 name {body} cid_transform attr_transform mark
val strg = XML.string_of (hd (Latex.output text))
val file = {path = Path.make [oid ^ "_snippet.tex"],
pos = @{here},
content = strg}
content = Bytes.string strg}
val _ = Generated_Files.write_file (Path.make ["latex_test"])
file
@ -125,7 +125,7 @@ val _ =
\<close>
ML\<open>open Bytes\<close>
text\<open>And here a tex - text macro.\<close>
text\<open>Pythons ReStructuredText (RST).
@{url \<open>https://de.wikipedia.org/wiki/ReStructuredText\<close>}. Tool: Sphinx.
@ -436,7 +436,7 @@ fun figure_antiq (check: Proof.context -> Path.T option -> Input.source -> Path.
else error "scale out of range (must be between 1 and 100"
val fig_args = Library.enclose "[" "]" (commas [wdth_ltx,scl_ltx])
val _ = writeln cap
fun proportion () = "0."^ (Int.toString (100 div length(!figure_proportions)))
fun proportion () = "0."^ (Int.toString (100 div List.length(!figure_proportions)))
\<comment> \<open>naive: assumes equal proportions\<close>
fun core arg = "\n\\centering\n"
^"\\includegraphics"