1 |
|
2 structure OutputFN = |
|
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 datatype entry = |
|
12 No_Entry |
|
13 | Code_Entry of string |
|
14 | String_Entry of string |
|
15 |
|
16 val index = ref No_Entry |
|
17 |
|
18 fun string_entry s = prefix ("\\index{" ^ s ^ "}") |
|
19 fun code_entry s = prefix ("\\index{" ^ s ^ "@{\\tt\\slshape{}" ^ s ^ "}}") |
|
20 |
|
21 fun get_word str = |
|
22 let |
|
23 fun only_letters [] = true |
|
24 | only_letters (x::xs) = |
|
25 if (Symbol.is_ascii_blank x) then false else only_letters xs |
|
26 in |
|
27 if (only_letters (Symbol.explode str)) then str |
|
28 else error ("Underspecified index entry only for single words allowed! Error with " ^ str) |
|
29 end |
|
30 |
|
31 fun index_entry entry txt = |
|
32 case entry of |
|
33 No_Entry => I |
|
34 | String_Entry "" => string_entry (get_word (implode txt)) |
|
35 | String_Entry s => string_entry s |
|
36 | Code_Entry "" => code_entry (get_word (implode txt)) |
|
37 | Code_Entry s => code_entry s |
|
38 |
|
39 |
|
40 fun translate f = Symbol.explode #> map f #> implode; |
|
41 |
|
42 val clean_string = translate |
|
43 (fn "_" => "\\_" |
|
44 | c => c); |
|
45 |
|
46 fun output txt = |
|
47 let |
|
48 val prts = map Pretty.str txt |
|
49 in |
|
50 prts |
|
51 |> (if ! ThyOutput.quotes then map Pretty.quote else I) |
|
52 |> (if ! ThyOutput.display then |
|
53 map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent)) |
|
54 #> space_implode "\\isasep\\isanewline%\n" |
|
55 #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) |
|
56 #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) |
|
57 #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
|
58 #> index_entry (!index) txt |
|
59 else |
|
60 map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of)) |
|
61 #> space_implode "\\isasep\\isanewline%\n" |
|
62 #> enclose "\\isa{" "}" |
|
63 #> index_entry (!index) txt) |
|
64 end |
|
65 |
|
66 |
|
67 fun boolean "" = true |
|
68 | boolean "true" = true |
|
69 | boolean "false" = false |
|
70 | boolean s = error ("Bad boolean value: " ^ quote s); |
|
71 |
|
72 val _ = ThyOutput.add_options |
|
73 [("gray", Library.setmp gray o boolean), |
|
74 ("linenos", Library.setmp linenos o boolean), |
|
75 ("index", Library.setmp index o String_Entry o clean_string), |
|
76 ("indexc", Library.setmp index o Code_Entry o clean_string)] |
|
77 |
|
78 |
|
79 end |
|