equal
deleted
inserted
replaced
24 else |
24 else |
25 map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of)) |
25 map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of)) |
26 #> space_implode "\\isasep\\isanewline%\n" |
26 #> space_implode "\\isasep\\isanewline%\n" |
27 #> enclose "\\isa{" "}"); |
27 #> enclose "\\isa{" "}"); |
28 |
28 |
|
29 fun output pretty src ctxt = output_list pretty src ctxt o single |
|
30 |
29 val _ = ThyOutput.add_options |
31 val _ = ThyOutput.add_options |
30 [("gray", Library.setmp gray o boolean)] |
32 [("gray", Library.setmp gray o boolean)] |
|
33 |
|
34 |
|
35 |
31 |
36 |
32 (** theory data **) |
37 (** theory data **) |
33 |
38 |
34 structure ChunkData = TheoryDataFun |
39 structure ChunkData = TheoryDataFun |
35 ( |
40 ( |