equal
deleted
inserted
replaced
58 val expressionN: string val expression: string -> T |
58 val expressionN: string val expression: string -> T |
59 val citationN: string val citation: string -> T |
59 val citationN: string val citation: string -> T |
60 val pathN: string val path: string -> T |
60 val pathN: string val path: string -> T |
61 val urlN: string val url: string -> T |
61 val urlN: string val url: string -> T |
62 val docN: string val doc: string -> T |
62 val docN: string val doc: string -> T |
63 val theory_exportsN: string val theory_exports: string -> T |
|
64 val markupN: string |
63 val markupN: string |
65 val consistentN: string |
64 val consistentN: string |
66 val unbreakableN: string |
65 val unbreakableN: string |
67 val block_properties: string list |
66 val block_properties: string list |
68 val indentN: string |
67 val indentN: string |
191 val no_reportN: string val no_report: T |
190 val no_reportN: string val no_report: T |
192 val badN: string val bad: unit -> T |
191 val badN: string val bad: unit -> T |
193 val intensifyN: string val intensify: T |
192 val intensifyN: string val intensify: T |
194 val browserN: string |
193 val browserN: string |
195 val graphviewN: string |
194 val graphviewN: string |
|
195 val theory_exportsN: string |
196 val sendbackN: string |
196 val sendbackN: string |
197 val paddingN: string |
197 val paddingN: string |
198 val padding_line: Properties.entry |
198 val padding_line: Properties.entry |
199 val padding_command: Properties.entry |
199 val padding_command: Properties.entry |
200 val dialogN: string val dialog: serial -> string -> T |
200 val dialogN: string val dialog: serial -> string -> T |
372 (* external resources *) |
372 (* external resources *) |
373 |
373 |
374 val (pathN, path) = markup_string "path" nameN; |
374 val (pathN, path) = markup_string "path" nameN; |
375 val (urlN, url) = markup_string "url" nameN; |
375 val (urlN, url) = markup_string "url" nameN; |
376 val (docN, doc) = markup_string "doc" nameN; |
376 val (docN, doc) = markup_string "doc" nameN; |
377 val (theory_exportsN, theory_exports) = markup_string "theory_exports" nameN; |
|
378 |
377 |
379 |
378 |
380 (* pretty printing *) |
379 (* pretty printing *) |
381 |
380 |
382 val markupN = "markup"; |
381 val markupN = "markup"; |
629 |
628 |
630 (* active areas *) |
629 (* active areas *) |
631 |
630 |
632 val browserN = "browser" |
631 val browserN = "browser" |
633 val graphviewN = "graphview"; |
632 val graphviewN = "graphview"; |
|
633 val theory_exportsN = "theory_exports"; |
634 |
634 |
635 val sendbackN = "sendback"; |
635 val sendbackN = "sendback"; |
636 val paddingN = "padding"; |
636 val paddingN = "padding"; |
637 val padding_line = (paddingN, "line"); |
637 val padding_line = (paddingN, "line"); |
638 val padding_command = (paddingN, "command"); |
638 val padding_command = (paddingN, "command"); |