equal
deleted
inserted
replaced
1 |
1 |
2 structure OutputTutorial = |
2 structure OutputTutorial = |
3 struct |
3 struct |
4 |
4 |
5 (* rebuilding the output function from ThyOutput in order to *) |
5 (* rebuilding the output function from ThyOutput in order to *) |
6 (* enable the options [gray, linenos, index] *) |
6 (* enable the options [gray, linenos, index] *) |
7 |
7 |
8 val gray = ref false |
8 val gray = ref false |
9 val linenos = ref false |
9 val linenos = ref false |
10 |
10 |
11 fun output txt = |
11 fun output txt = |
24 map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of)) |
24 map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of)) |
25 #> space_implode "\\isasep\\isanewline%\n" |
25 #> space_implode "\\isasep\\isanewline%\n" |
26 #> enclose "\\isa{" "}") |
26 #> enclose "\\isa{" "}") |
27 end |
27 end |
28 |
28 |
|
29 |
29 datatype qstring = |
30 datatype qstring = |
30 NoString |
31 NoString |
31 | Plain of string |
32 | Plain of string |
32 | Code of string |
33 | Code of string |
33 | IStruc of string |
34 | IStruct of string |
34 |
35 |
35 datatype entry = |
36 datatype entry = |
36 No_Entry |
37 No_Entry |
37 | Default |
38 | Default |
38 | Explicit of string |
39 | Explicit of string |
65 end |
66 end |
66 |
67 |
67 fun get_qstring NoString = "" |
68 fun get_qstring NoString = "" |
68 | get_qstring (Plain s) = get_word s |
69 | get_qstring (Plain s) = get_word s |
69 | get_qstring (Code s) = let val w = get_word s in (w ^ "@{\\tt\\slshape{}" ^ w ^ "}") end |
70 | get_qstring (Code s) = let val w = get_word s in (w ^ "@{\\tt\\slshape{}" ^ w ^ "}") end |
70 | get_qstring (IStruc s) = "in {\\tt\\slshape{}" ^ (get_word s) ^ "}" |
71 | get_qstring (IStruct s) = "in {\\tt\\slshape{}" ^ (get_word s) ^ "}" |
71 |
72 |
72 fun is_empty_qstr (Plain "") = true |
73 fun is_empty_qstr (Plain "") = true |
73 | is_empty_qstr (Code "") = true |
74 | is_empty_qstr (Code "") = true |
74 | is_empty_qstr _ = false |
75 | is_empty_qstr _ = false |
75 |
76 |