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 |
|
438
|
5 |
(* rebuilding the output function from Thy_Output 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 |
|
449
|
12 |
fun output ctxt txt =
|
255
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
|
449
|
17 |
|> (if Config.get ctxt Thy_Output.quotes then map Pretty.quote else I)
|
|
18 |
|> (if Config.get ctxt Thy_Output.display then
|
|
19 |
map (Output.output o Pretty.string_of o Pretty.indent (Config.get ctxt Thy_Output.indent))
|
255
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
|
449
|
25 |
map (Output.output o (if Config.get ctxt Thy_Output.break then Pretty.string_of else Pretty.str_of))
|
255
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 |
|
373
|
72 |
fun get_str_index {main = m, minor = n} =
|
|
73 |
(case n of
|
|
74 |
Struct s => implode ["\\index[str]{{\\tt\\slshape{}", get_word s, "}!", get_indstring m, "}"]
|
|
75 |
| _ => "")
|
|
76 |
|
449
|
77 |
fun output_indexed ctxt ind txt =
|
|
78 |
txt |> output ctxt
|
316
|
79 |
|> prefix (get_index ind)
|
373
|
80 |
|> prefix (get_str_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
|
81 |
|
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
82 |
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
|
83 |
| 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
|
84 |
| 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
|
85 |
| 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
|
86 |
|
471
|
87 |
val gray_setup = Thy_Output.add_option @{binding "gray"}
|
449
|
88 |
(Thy_Output.add_wrapper o Library.setmp_CRITICAL gray o boolean)
|
471
|
89 |
val linenos_setup = Thy_Output.add_option @{binding "linenos"}
|
449
|
90 |
(Thy_Output.add_wrapper o 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
|
91 |
|
471
|
92 |
val setup =
|
|
93 |
gray_setup #>
|
|
94 |
linenos_setup
|
|
95 |
|
255
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
96 |
end |