nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Eingeführter title etc. …

This commit is contained in:
Burkhart Wolff 2018-06-11 17:35:12 +02:00
parent 19959304d4
commit ab127abe9a
1 changed files with 28 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
Isa_DOF.thy
View File

@ -14,8 +14,11 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *)
Assert
keywords "+=" ":="
and "section*" "subsection*" "subsubsection*"
"paragraph*" "subparagraph*" "text*" ::thy_decl
and "title*" "subtitle*"
"section*" "subsection*" "subsubsection*"
"figure*" "side_by_side_figure*"
"paragraph*" "subparagraph*"
"text*" :: thy_decl
and "open_monitor*" "close_monitor*" "declare_reference*"
"update_instance*" "doc_class" ::thy_decl
@ -501,11 +504,23 @@ fun update_instance_command (((oid:string,pos),cid_pos),
in Toplevel.theory(upd)
end
val _ =
Outer_Syntax.command ("title*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
val _ =
Outer_Syntax.command ("subtitle*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
val _ =
Outer_Syntax.command ("section*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
val _ =
Outer_Syntax.command ("subsection*", @{here}) "subsection heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
@ -526,6 +541,17 @@ val _ =
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
val _ =
Outer_Syntax.command ("figure*", @{here}) "paragraph heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
val _ =
Outer_Syntax.command ("side_by_side_figure*", @{here}) "paragraph heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
val _ =
Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)"
(attributes -- Parse.opt_target -- Parse.document_source