78 ((subparagraphN, @{here}), SOME ((Keyword.document_heading, []), [])), |
78 ((subparagraphN, @{here}), SOME ((Keyword.document_heading, []), [])), |
79 ((textN, @{here}), SOME ((Keyword.document_body, []), [])), |
79 ((textN, @{here}), SOME ((Keyword.document_body, []), [])), |
80 ((txtN, @{here}), SOME ((Keyword.document_body, []), [])), |
80 ((txtN, @{here}), SOME ((Keyword.document_body, []), [])), |
81 ((text_rawN, @{here}), SOME ((Keyword.document_raw, []), [])), |
81 ((text_rawN, @{here}), SOME ((Keyword.document_raw, []), [])), |
82 ((theoryN, @{here}), SOME ((Keyword.thy_begin, []), ["theory"])), |
82 ((theoryN, @{here}), SOME ((Keyword.thy_begin, []), ["theory"])), |
83 (("ML_file", @{here}), SOME ((Keyword.thy_load, []), ["ML"])), |
83 (("ML", @{here}), SOME ((Keyword.thy_decl, []), ["ML"]))]; |
84 (("ML_file_debug", @{here}), SOME ((Keyword.thy_load, []), ["ML"])), |
|
85 (("ML_file_no_debug", @{here}), SOME ((Keyword.thy_load, []), ["ML"]))]; |
|
86 |
84 |
87 |
85 |
88 (* theory data *) |
86 (* theory data *) |
89 |
87 |
90 structure Data = Theory_Data |
88 structure Data = Theory_Data |