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