255
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
|
256
|
2 |
structure OutputTutorial =
|
255
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
struct
|
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
|
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
(* rebuilding the output function from ThyOutput in order to *)
|
316
|
6 |
(* enable the options [gray, linenos] *)
|
255
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
|
328
|
8 |
val gray = Unsynchronized.ref false
|
|
9 |
val linenos = Unsynchronized.ref false
|
255
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
|
311
|
11 |
|
255
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
fun output txt =
|
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
let
|
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
val prts = map Pretty.str txt
|
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
15 |
in
|
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
prts
|
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
17 |
|> (if ! ThyOutput.quotes then map Pretty.quote else I)
|
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
18 |
|> (if ! ThyOutput.display then
|
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
19 |
map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent))
|
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
20 |
#> space_implode "\\isasep\\isanewline%\n"
|
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
21 |
#> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I)
|
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
22 |
#> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I)
|
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
23 |
#> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
|
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
24 |
else
|
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
25 |
map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of))
|
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
26 |
#> space_implode "\\isasep\\isanewline%\n"
|
256
|
27 |
#> enclose "\\isa{" "}")
|
255
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
28 |
end
|
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
29 |
|
316
|
30 |
datatype indstring =
|
258
|
31 |
NoString
|
302
|
32 |
| Plain of string
|
|
33 |
| Code of string
|
316
|
34 |
| Struct of string
|
256
|
35 |
|
316
|
36 |
fun translate_string f = Symbol.explode #> map f #> implode;
|
256
|
37 |
|
316
|
38 |
val clean_string = translate_string
|
256
|
39 |
(fn "_" => "\\_"
|
|
40 |
| "#" => "\\#"
|
|
41 |
| "<" => "\\isacharless"
|
|
42 |
| ">" => "\\isachargreater"
|
|
43 |
| "{" => "\\{"
|
|
44 |
| "|" => "\\isacharbar"
|
|
45 |
| "}" => "\\}"
|
|
46 |
| "$" => "\\isachardollar"
|
|
47 |
| "!" => "\\isacharbang"
|
261
|
48 |
| "\<dash>" => "-"
|
316
|
49 |
| c => c)
|
256
|
50 |
|
|
51 |
fun get_word str =
|
|
52 |
let
|
|
53 |
fun only_letters [] = true
|
|
54 |
| only_letters (x::xs) =
|
|
55 |
if (Symbol.is_ascii_blank x) then false else only_letters xs
|
|
56 |
in
|
316
|
57 |
if only_letters (Symbol.explode str)
|
|
58 |
then clean_string str
|
|
59 |
else error ("Only single word allowed! Error with " ^ quote str)
|
256
|
60 |
end
|
|
61 |
|
316
|
62 |
fun get_indstring NoString = ""
|
|
63 |
| get_indstring (Plain s) = get_word s
|
|
64 |
| get_indstring (Code s) = let val w = get_word s in implode[w, "@{\\tt\\slshape{}", w, "}"] end
|
|
65 |
| get_indstring (Struct s) = implode ["in {\\tt\\slshape{}", get_word s, "}"]
|
256
|
66 |
|
316
|
67 |
fun get_index {main = m, minor = n} =
|
258
|
68 |
(if n = NoString
|
316
|
69 |
then implode ["\\index{", get_indstring m, "}"]
|
|
70 |
else implode ["\\index{", get_indstring m, " (", get_indstring n, ")}"])
|
256
|
71 |
|
316
|
72 |
fun output_indexed ind txt =
|
256
|
73 |
txt |> output
|
316
|
74 |
|> prefix (get_index ind)
|
255
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
75 |
|
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
76 |
fun boolean "" = true
|
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
77 |
| boolean "true" = true
|
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
78 |
| boolean "false" = false
|
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
79 |
| boolean s = error ("Bad boolean value: " ^ quote s);
|
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
80 |
|
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
81 |
val _ = ThyOutput.add_options
|
351
|
82 |
[("gray", Library.setmp_CRITICAL gray o boolean),
|
|
83 |
("linenos", Library.setmp_CRITICAL linenos o boolean)]
|
255
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
84 |
|
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
85 |
end |