diff --git a/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy b/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy index af2f6be..c8b4527 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy @@ -41,20 +41,20 @@ text\ IDE support. \ -(* should be text* *) -text -\ - -\begin{sml} -structure Data = Generic_Data +(* should work as text*, but doesn't. *) +(* +text*[xxx::SML] +\structure Data = Generic_Data ( type T = docobj_tab * docclass_tab * ... val empty = (initial_docobj_tab, initial_docclass_tab, ...) val extend = I fun merge((d1,c1,...),(d2,c2,...)) = (merge_docobj_tab (d1,d2,...), merge_docclass_tab(c1,c2,...)) ); -\end{sml} \ +*) + + section\\isadof: A User-Defined Plugin in Isabelle/Isar\ text\ diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 2cff442..a1b322d 100755 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -652,7 +652,7 @@ fun print_docclass_template cid ctxt = |filter_overrides ((ln,s)::S) = (ln,s):: filter_overrides(filter(fn(_,s')=> s<>s')S) val hierarchy = map (fn(ln,s)=>ln^"."^s)(filter_overrides(flatten_hrchy brute_hierarchy)) val args = String.concatWith "=%\n , " (" label=,type":: hierarchy); - val template = "\\newisadof{"^cid_long^"}%\n["^args^"][1]\n{%\n#1%\n}\n\n"; + val template = "\\newisadof{"^cid_long^"}%\n["^args^"=%\n][1]\n{%\n#1%\n}\n\n"; in writeln template end; diff --git a/src/ontologies/technical_report/DOF-technical_report.sty b/src/ontologies/technical_report/DOF-technical_report.sty index 0a5838b..a853fd4 100755 --- a/src/ontologies/technical_report/DOF-technical_report.sty +++ b/src/ontologies/technical_report/DOF-technical_report.sty @@ -33,3 +33,22 @@ % \usepackage{xcolor} % \usepackage{lstisadof-manual} +\newisadof{text.technical_report.SML}% +[ label=,type=% + , Isa_COL.text_element.level=% + , Isa_COL.text_element.referentiable=% + , Isa_COL.text_element.variants=% + , scholarly_paper.text_section.main_author=% + , scholarly_paper.text_section.fixme_list=% + , scholarly_paper.technical.definition_list=% + , scholarly_paper.technical.status=% + , scholarly_paper.technical.formal_results=% + , technical_report.code.checked=% + , technical_report.code.caption=% +] +[1] +{% +\begin{sml}% +#1 +\end{sml}% +} diff --git a/src/ontologies/technical_report/technical_report.thy b/src/ontologies/technical_report/technical_report.thy index 61e801f..a1d1c23 100755 --- a/src/ontologies/technical_report/technical_report.thy +++ b/src/ontologies/technical_report/technical_report.thy @@ -59,6 +59,7 @@ doc_class "ISAR" = code + doc_class "LATEX" = code + checked :: bool <= "False" +print_doc_class_template "SML" (* just a sample *) doc_class report =