|
1 |
|
2 structure OutputTutorial = |
|
3 struct |
|
4 |
|
5 (* rebuilding the output function from ThyOutput in order to *) |
|
6 (* enable the options [gray, linenos, index] *) |
|
7 |
|
8 val gray = ref false |
|
9 val linenos = ref false |
|
10 |
|
11 fun output txt = |
|
12 let |
|
13 val prts = map Pretty.str txt |
|
14 in |
|
15 prts |
|
16 |> (if ! ThyOutput.quotes then map Pretty.quote else I) |
|
17 |> (if ! ThyOutput.display then |
|
18 map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent)) |
|
19 #> space_implode "\\isasep\\isanewline%\n" |
|
20 #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) |
|
21 #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) |
|
22 #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
|
23 else |
|
24 map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of)) |
|
25 #> space_implode "\\isasep\\isanewline%\n" |
|
26 #> enclose "\\isa{" "}") |
|
27 end |
|
28 |
|
29 datatype qstring = |
|
30 Plain of string |
|
31 | Code of string |
|
32 |
|
33 datatype entry = |
|
34 No_Entry |
|
35 | Default |
|
36 | Explicit of string |
|
37 |
|
38 val index = ref No_Entry |
|
39 |
|
40 fun translate f = Symbol.explode #> map f #> implode; |
|
41 |
|
42 val clean_string = translate |
|
43 (fn "_" => "\\_" |
|
44 | "#" => "\\#" |
|
45 | "<" => "\\isacharless" |
|
46 | ">" => "\\isachargreater" |
|
47 | "{" => "\\{" |
|
48 | "|" => "\\isacharbar" |
|
49 | "}" => "\\}" |
|
50 | "$" => "\\isachardollar" |
|
51 | "!" => "\\isacharbang" |
|
52 | "\\<dash>" => "-" |
|
53 | c => c); |
|
54 |
|
55 fun get_word str = |
|
56 let |
|
57 fun only_letters [] = true |
|
58 | only_letters (x::xs) = |
|
59 if (Symbol.is_ascii_blank x) then false else only_letters xs |
|
60 in |
|
61 if (only_letters (Symbol.explode str)) then (clean_string str) |
|
62 else error ("Underspecified index entry only for single words allowed! Error with " ^ quote str) |
|
63 end |
|
64 |
|
65 fun get_qstring (Plain s) = get_word s |
|
66 | get_qstring (Code s) = let val w = get_word s in (w ^ "@{\\tt\\slshape{}" ^ w ^ "}") end |
|
67 |
|
68 fun is_empty_qstr (Plain "") = true |
|
69 | is_empty_qstr (Code "") = true |
|
70 | is_empty_qstr _ = false |
|
71 |
|
72 fun get_index_info {main = m, minor = n} = |
|
73 (if n = "" |
|
74 then "\\index{" ^ (get_qstring m) ^ "}" |
|
75 else "\\indexdef{" ^ (get_qstring m) ^ "}{" ^ n ^ "}") |
|
76 |
|
77 fun index_entry entry index_info = |
|
78 case entry of |
|
79 No_Entry => I |
|
80 | Explicit s => prefix s |
|
81 | Default => prefix (get_index_info index_info) |
|
82 |
|
83 fun output_indexed txt index_info = |
|
84 txt |> output |
|
85 |> index_entry (!index) index_info |
|
86 |
|
87 fun boolean "" = true |
|
88 | boolean "true" = true |
|
89 | boolean "false" = false |
|
90 | boolean s = error ("Bad boolean value: " ^ quote s); |
|
91 |
|
92 fun explicit "" = Default |
|
93 | explicit s = Explicit s |
|
94 |
|
95 val _ = ThyOutput.add_options |
|
96 [("gray", Library.setmp gray o boolean), |
|
97 ("linenos", Library.setmp linenos o boolean), |
|
98 ("index", Library.setmp index o explicit)] |
|
99 |
|
100 |
|
101 end |