From 803e97ce16605e08314813f0f2f8261128fb2aea Mon Sep 17 00:00:00 2001 From: bu Date: Tue, 14 May 2019 09:13:42 +0200 Subject: [PATCH] Experiments with the LaTeX generator --- Isa_COL.thy | 2 +- Isa_DOF.thy | 17 +++++---- ROOT | 2 +- ROOTS | 1 - examples/conceptual/Attributes.thy | 2 +- examples/conceptual/Concept_Example.thy | 2 +- ontologies/Conceptual.thy | 2 +- patches/thy_output.ML | 46 +++++++++++++++++++++++-- 8 files changed, 59 insertions(+), 15 deletions(-) delete mode 100644 ROOTS diff --git a/Isa_COL.thy b/Isa_COL.thy index db3f53a..76e5469 100644 --- a/Isa_COL.thy +++ b/Isa_COL.thy @@ -5,7 +5,7 @@ text\ Offering \<^item> \<^item> LaTeX support. \ - + theory Isa_COL imports Isa_DOF begin diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 50f74d2..cac44be 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -46,7 +46,7 @@ begin text\ @{footnote \sdf\}, @{file "$ISABELLE_HOME/src/Pure/ROOT.ML"}\ - +ML_file "patches/thy_output.ML"; section\Primitive Markup Generators\ ML\ @@ -109,7 +109,7 @@ fun holstring_to_bstring ctxt (x:string) : bstring = section\ A HomeGrown Document Type Management (the ''Model'') \ -ML\ +ML\ structure DOF_core = struct @@ -1534,8 +1534,11 @@ end *) val _ = Thy_Output.set_meta_args_parser - (fn thy => (Scan.optional ( ODL_Command_Parser.attributes - >> meta_args_2_string thy) "")) + (fn thy => let val _ = writeln "META_ARGS_PARSING" + in + (Scan.optional ( ODL_Command_Parser.attributes + >> meta_args_2_string thy) "") + end) end @@ -1685,10 +1688,10 @@ val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Args.text_input) fun pretty_docitem_antiquotation_generic cid_decl ctxt ({unchecked = x, define = y}, src ) = - let val _ = check_and_mark ctxt cid_decl + let val _ = writeln ("ZZZ" ^ Input.source_content src ^ "::2::" ^ cid_decl) + val _ = check_and_mark ctxt cid_decl ({strict_checking = not x}) - (Input.pos_of src) (Input.source_content src) - val _ = writeln ("ZZZ" ^ Input.source_content src ^ "::" ^ cid_decl) + (Input.pos_of src) (Input.source_content src) in (if y then Latex.enclose_block "\\label{" "}" else Latex.enclose_block "\\autoref{" "}") [Latex.string (Input.source_content src)] diff --git a/ROOT b/ROOT index a975506..7d8ca96 100644 --- a/ROOT +++ b/ROOT @@ -4,8 +4,8 @@ session "Isabelle_DOF" = "Functional-Automata" + "Regular-Sets" theories Isa_DOF - "ontologies/CENELEC_50128" "ontologies/Conceptual" + "ontologies/CENELEC_50128" "ontologies/scholarly_paper" "ontologies/technical_report" "ontologies/mathex_onto" diff --git a/ROOTS b/ROOTS deleted file mode 100644 index 1e107f5..0000000 --- a/ROOTS +++ /dev/null @@ -1 +0,0 @@ -examples diff --git a/examples/conceptual/Attributes.thy b/examples/conceptual/Attributes.thy index 4378a73..84f381c 100644 --- a/examples/conceptual/Attributes.thy +++ b/examples/conceptual/Attributes.thy @@ -16,7 +16,7 @@ val {docobj_tab={tab = docitem_tab, ...},docclass_tab, ISA_transformer_tab, moni Symtab.dest docitem_tab; Symtab.dest docclass_tab; \ - + ML\ fun fac x = if x = 0 then 1 else x * (fac(x -1)); fac 3; diff --git a/examples/conceptual/Concept_Example.thy b/examples/conceptual/Concept_Example.thy index 004152a..a8b8c6a 100644 --- a/examples/conceptual/Concept_Example.thy +++ b/examples/conceptual/Concept_Example.thy @@ -14,7 +14,7 @@ section*[a::A, x = "3"] \ Lorem ipsum dolor sit amet, ... \ text*[c1::C, x = "''beta''"] \ ... suspendisse non arcu malesuada mollis, nibh morbi, ... \ text*[d::D, a1 = "X3"] \ ... phasellus amet id massa nunc, pede suscipit repellendus, - ... @{docitem c1} @{thm "refl"}\ + ... @{docitem "c1"} @{thm "refl"} \ update_instance*[d::D, a1 := X2] diff --git a/ontologies/Conceptual.thy b/ontologies/Conceptual.thy index 6f587c1..1f60bc2 100644 --- a/ontologies/Conceptual.thy +++ b/ontologies/Conceptual.thy @@ -54,4 +54,4 @@ text*[sdfg] {* fg @{thm refl}*} text*[xxxy] {* dd @{docitem \sdfg\} @{thm refl}*} -end \ No newline at end of file +end diff --git a/patches/thy_output.ML b/patches/thy_output.ML index dcc1746..567a1b7 100644 --- a/patches/thy_output.ML +++ b/patches/thy_output.ML @@ -174,12 +174,21 @@ val is_black_comment = Token.is_formal_comment; (* presentation tokens *) +(* orig Isabelle 2018 datatype token = Ignore_Token | Basic_Token of Token.T | Markup_Token of string * Input.source | Markup_Env_Token of string * Input.source | Raw_Token of Input.source; +*) + +datatype token = + Ignore_Token + | Basic_Token of Token.T + | Markup_Token of string * string * Input.source + | Markup_Env_Token of string * string * Input.source + | Raw_Token of Input.source; fun basic_token pred (Basic_Token tok) = pred tok | basic_token _ _ = false; @@ -189,6 +198,7 @@ val white_comment_token = basic_token is_white_comment; val blank_token = basic_token Token.is_blank; val newline_token = basic_token Token.is_newline; +(* orig Isabelle 2018 fun present_token ctxt tok = (case tok of Ignore_Token => [] @@ -201,6 +211,21 @@ fun present_token ctxt tok = | Raw_Token source => Latex.string "%\n" :: output_document ctxt {markdown = true} source @ [Latex.string "\n"]); +*) + +(* modified by bu: added meta_args; currently ignored*) +fun present_token ctxt tok = + (case tok of + Ignore_Token => [] + | Basic_Token tok => output_token ctxt tok + | Markup_Token (cmd, meta_args, source) => + Latex.enclose_body ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n" + (output_document ctxt {markdown = false} source) + | Markup_Env_Token (cmd, meta_args,source) => + [Latex.environment_block ("isamarkup" ^ cmd) (output_document ctxt {markdown = true} source)] + | Raw_Token source => + Latex.string "%\n" :: output_document ctxt {markdown = true} source @ [Latex.string "\n"]); + (* command spans *) @@ -381,6 +406,7 @@ fun present_thy options thy (segments: segment list) = val ignored = Scan.state --| ignore >> (fn d => (NONE, (Ignore_Token, ("", d)))); + (* orig Isabelle 2018 fun markup pred mk flag = Scan.peek (fn d => improper |-- Parse.position (Scan.one (fn tok => @@ -390,6 +416,22 @@ fun present_thy options thy (segments: segment list) = >> (fn (((tok, pos'), tags), source) => let val name = Token.content_of tok in (SOME (name, pos', tags), (mk (name, source), (flag, d))) end)); + *) + + fun markup pred mk flag = Scan.peek (fn d => + improper |-- + Parse.position (Scan.one (fn tok => Token.is_command tok andalso + pred keywords (Token.content_of tok))) -- + Scan.repeat tag -- + (improper |-- + (Parse.!!!! + ( (!meta_args_parser_hook thy) + -- ( (improper -- locale -- improper) + |-- (Parse.document_source)) + --| improper_end))) + >> (fn (((tok, pos'), tags), (meta_args,source)) => + let val name = Token.content_of tok + in (SOME (name, pos', tags), (mk (name, meta_args, source), (flag, d))) end)); val command = Scan.peek (fn d => Scan.optional (Scan.one Token.is_command_modifier ::: improper) [] -- @@ -405,7 +447,7 @@ fun present_thy options thy (segments: segment list) = val cmt = Scan.peek (fn d => (Parse.$$$ "--" || Parse.$$$ Symbol.comment) |-- Parse.!!!! (improper |-- Parse.document_source) >> - (fn source => (NONE, (Markup_Token ("cmt", source), ("", d))))); + (fn source => (NONE, (Markup_Token ("cmt", "", source), ("", d))))); val other = Scan.peek (fn d => @@ -415,7 +457,7 @@ fun present_thy options thy (segments: segment list) = (ignored || markup Keyword.is_document_heading Markup_Token markup_true || markup Keyword.is_document_body Markup_Env_Token markup_true || - markup Keyword.is_document_raw (Raw_Token o #2) "") >> single || + markup Keyword.is_document_raw (Raw_Token o #3) "") >> single || command || (cmt || other) >> single;