Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Quick fix for text* macros latex output
ci/woodpecker/push/build Pipeline was successful Details

This commit is contained in:
Nicolas Méric 2023-04-07 07:00:56 +02:00
parent cb2b0dc230
commit 36cd3817cf
4 changed files with 72 additions and 39 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
Isabelle_DOF-Unit-Tests/AssnsLemmaThmEtc.thy
View File

@ -43,7 +43,7 @@ text\<open>For now, as the term annotation is not bound to a meta logic which wi
\<^term>\<open>[@{term ''True''}]\<close> to \<^term>\<open>[True]\<close>, we can not use the HOL \<^const>\<open>True\<close> constant
in the assertion.\<close>
ML\<open> @{term "[@{term \<open>True \<longrightarrow> True \<close>}]"}; (* with isa-check *) \<close>
ML\<open> @{term_ "[@{term \<open>True \<longrightarrow> True \<close>}]"}; (* with isa-check *) \<close>
ML\<open>
(* Checking the default classes which should be in a neutral(unset) state. *)
@ -64,7 +64,7 @@ ML\<open>
\<close>
Definition*[e1::"definition"]\<open>Lorem ipsum dolor sit amet, ... \<close>
Definition*[e1]\<open>Lorem ipsum dolor sit amet, ... \<close>
text\<open>Note that this should yield a warning since \<^theory_text>\<open>Definition*\<close> uses as "implicit default" the class
\<^doc_class>\<open>math_content\<close> which has no \<^term>\<open>text_element.level\<close> set, however in this context,
it is required to be a positive number since it is \<^term>\<open>text_element.referentiable\<close> .

31
Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy
View File

@ -53,12 +53,12 @@ ML\<open>
val _ =
Monitor_Command_Parser.document_command \<^command_keyword>\<open>abstract*\<close> "Textual Definition"
{markdown = true, body = true}
(Onto_Macros.enriched_document_cmd_exp (SOME "abstract") []);
(Onto_Macros.enriched_document_cmd_exp (SOME "abstract") []) (K(K I));
val _ =
Monitor_Command_Parser.document_command \<^command_keyword>\<open>author*\<close> "Textual Definition"
{markdown = true, body = true}
(Onto_Macros.enriched_document_cmd_exp (SOME "author") []);
(Onto_Macros.enriched_document_cmd_exp (SOME "author") []) (K(K I));
\<close>
text\<open>Scholarly Paper is oriented towards the classical domains in science:
@ -444,48 +444,49 @@ fun doc_cmd kwd txt flag key =
in
Onto_Macros.enriched_formal_statement_command default [("mcc",key)] meta_args thy
end)
(Onto_Macros.transform_attr [("mcc",key)])
in
val _ = doc_cmd \<^command_keyword>\<open>Definition*\<close> "Freeform Definition"
Definition_default_class \<^const_name>\<open>defn\<close>;
Definition_default_class "defn";
val _ = doc_cmd \<^command_keyword>\<open>Lemma*\<close> "Freeform Lemma Description"
Lemma_default_class \<^const_name>\<open>lemm\<close>;
Lemma_default_class "lemm";
val _ = doc_cmd \<^command_keyword>\<open>Theorem*\<close> "Freeform Theorem"
Theorem_default_class \<^const_name>\<open>theom\<close>;
Theorem_default_class "theom";
(* cut and paste to make it runnable, but nonsensical so far: *)
val _ = doc_cmd \<^command_keyword>\<open>Proposition*\<close> "Freeform Proposition"
Proposition_default_class \<^const_name>\<open>prpo\<close>;
Proposition_default_class "prpo";
val _ = doc_cmd \<^command_keyword>\<open>Premise*\<close> "Freeform Premise"
Premise_default_class \<^const_name>\<open>prms\<close>;
Premise_default_class "prms";
val _ = doc_cmd \<^command_keyword>\<open>Corollary*\<close> "Freeform Corollary"
Corollary_default_class \<^const_name>\<open>corr\<close>;
Corollary_default_class "corr";
val _ = doc_cmd \<^command_keyword>\<open>Consequence*\<close> "Freeform Consequence"
Consequence_default_class \<^const_name>\<open>cons\<close>;
Consequence_default_class "cons";
val _ = doc_cmd \<^command_keyword>\<open>Conclusion*\<close> "Freeform Conclusion"
Conclusion_default_class \<^const_name>\<open>conc_stmt\<close>;
Conclusion_default_class "conc_stmt";
val _ = doc_cmd \<^command_keyword>\<open>Assumption*\<close> "Freeform Assumption"
Assumption_default_class \<^const_name>\<open>assm\<close>;
Assumption_default_class "assm";
val _ = doc_cmd \<^command_keyword>\<open>Hypothesis*\<close> "Freeform Hypothesis"
Hypothesis_default_class \<^const_name>\<open>prpo\<close>;
Hypothesis_default_class "prpo";
val _ = doc_cmd \<^command_keyword>\<open>Assertion*\<close> "Freeform Assertion"
Assertion_default_class \<^const_name>\<open>assn\<close>;
Assertion_default_class "assn";
val _ = doc_cmd \<^command_keyword>\<open>Proof*\<close> "Freeform Proof"
Proof_default_class \<^const_name>\<open>prf_stmt\<close>;
Proof_default_class "prf_stmt";
val _ = doc_cmd \<^command_keyword>\<open>Example*\<close> "Freeform Example"
Example_default_class \<^const_name>\<open>expl_stmt\<close>;
Example_default_class "expl_stmt";
end
end
\<close>

45
Isabelle_DOF/thys/Isa_COL.thy
View File

@ -103,13 +103,44 @@ fun transform_cid thy NONE X = X
end
in
fun enriched_formal_statement_command ncid (S: (string * string) list) =
let fun transform_attr doc_attrs = (map (fn(cat,tag) => ((cat,@{here}),tag)) S) @
(("formal_results",@{here}),"([]::thm list)")::doc_attrs
in fn margs => fn thy =>
fun transform_attr S cid_long thy doc_attrs =
let
fun transform_attr' [] doc_attrs = doc_attrs
| transform_attr' (s::S) (doc_attrs) =
let fun markup2string s = s |> YXML.content_of
|> Symbol.explode
|> List.filter (fn c => c <> Symbol.DEL)
|> String.concat
fun toLong n = DOF_core.get_attribute_info cid_long (markup2string n) thy
|> the |> #long_name
val (name', value) = s |> (fn (n, v) => (toLong n, v))
val doc_attrs' = doc_attrs
|> map (fn (name, term) => if name = name'
then (name, value)
else (name, term))
in if doc_attrs' = doc_attrs
then transform_attr' S doc_attrs' |> cons (name', value)
else transform_attr' S doc_attrs'
end
in transform_attr' S doc_attrs end
(*fun update_meta_args_attrs S
((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) =
(((oid, pos),cid_pos), transform_attr S doc_attrs)
*)
(*fun enriched_formal_statement_command ncid (S: (string * string) list) =
fn margs => fn thy =>
Monitor_Command_Parser.gen_enriched_document_cmd {inline=true}
(transform_cid thy ncid) transform_attr margs thy
end;
(transform_cid thy ncid) (transform_attr S) margs thy
*)
fun enriched_formal_statement_command ncid (S: (string * string) list) =
let fun transform_attr doc_attrs = (map (fn(cat,tag) => ((cat,@{here}),tag)) S) @
(("formal_results",@{here}),"([]::thm list)")::doc_attrs
in fn margs => fn thy =>
Monitor_Command_Parser.gen_enriched_document_cmd {inline=true}
(transform_cid thy ncid) transform_attr margs thy
end;
fun enriched_document_cmd_exp ncid (S: (string * string) list) =
(* expands ncid into supertype-check. *)
@ -123,7 +154,7 @@ end (* local *)
fun heading_command (name, pos) descr level =
Monitor_Command_Parser.document_command (name, pos) descr
{markdown = false, body = true} (enriched_text_element_cmd level);
{markdown = false, body = true} (enriched_text_element_cmd level) (K(K I));
val _ = heading_command \<^command_keyword>\<open>title*\<close> "section heading" NONE;
val _ = heading_command \<^command_keyword>\<open>subtitle*\<close> "section heading" NONE;

31
Isabelle_DOF/thys/Isa_DOF.thy
View File

@ -2137,17 +2137,15 @@ fun close_monitor_command (args as (((oid, pos), cid_pos),
end
fun meta_args_2_latex thy ((((lab, pos), cid_opt), attr_list) : ODL_Meta_Args_Parser.meta_args_t) =
fun meta_args_2_latex thy transform_attr
((((lab, pos), cid_opt), attr_list) : ODL_Meta_Args_Parser.meta_args_t) =
(* for the moment naive, i.e. without textual normalization of
attribute names and adapted term printing *)
let val l = DOF_core.get_instance_name_global lab thy |> enclose "{" "}"
|> prefix "label = "
(* val _ = writeln("meta_args_2_string lab:"^ lab ^":"^ (@{make_string } cid_opt) ) *)
val cid_long = case cid_opt of
NONE => let val DOF_core.Instance cid =
DOF_core.get_instance_global lab thy
in cid |> #cid end
NONE => DOF_core.cid_of lab thy
| SOME(cid,_) => DOF_core.get_onto_class_name_global' cid thy
(* val _ = writeln("meta_args_2_string cid_long:"^ cid_long ) *)
val cid_txt = "type = " ^ (enclose "{" "}" cid_long);
@ -2195,8 +2193,11 @@ fun meta_args_2_latex thy ((((lab, pos), cid_opt), attr_list) : ODL_Meta_Args_Pa
val default_args_filtered = filter (fn (a,_) => not (exists (fn b => b = a)
(map (fn (c,_) => c) actual_args))) default_args
val str_args = map (fn (lhs,rhs) => lhs^" = "^(enclose "{" "}" rhs))
(actual_args@default_args_filtered)
val transformed_args = (actual_args@default_args_filtered)
|> transform_attr cid_long thy
val str_args = transformed_args
|> map (fn (lhs,rhs) => lhs^" = "^(enclose "{" "}" rhs))
val label_and_type = String.concat [ l, ",", cid_txt]
val str_args = label_and_type::str_args
in
@ -2220,15 +2221,15 @@ fun gen_enriched_document_cmd' {inline} cid_transform attr_transform
(* {markdown = true} sets the parsing process such that in the text-core
markdown elements are accepted. *)
fun document_output {markdown: bool, markup: Latex.text -> Latex.text} meta_args text ctxt =
fun document_output {markdown: bool, markup: Latex.text -> Latex.text} transform_attr meta_args text ctxt =
let
val thy = Proof_Context.theory_of ctxt;
val _ = Context_Position.reports ctxt (Document_Output.document_reports text);
val output_meta = meta_args_2_latex thy meta_args;
val output_meta = meta_args_2_latex thy transform_attr meta_args;
val output_text = Document_Output.output_document ctxt {markdown = markdown} text;
in markup (output_meta @ output_text) end;
fun document_output_reports name {markdown, body} meta_args text ctxt =
fun document_output_reports name {markdown, body} transform_attr meta_args text ctxt =
let
(*val pos = Input.pos_of text;
val _ =
@ -2238,16 +2239,16 @@ fun document_output_reports name {markdown, body} meta_args text ctxt =
fun markup xml =
let val m = if body then Markup.latex_body else Markup.latex_heading
in [XML.Elem (m (Latex.output_name name), xml)] end;
in document_output {markdown = markdown, markup = markup} meta_args text ctxt end;
in document_output {markdown = markdown, markup = markup} transform_attr meta_args text ctxt end;
(* document output commands *)
fun document_command (name, pos) descr mark cmd =
fun document_command (name, pos) descr mark cmd transform_attr =
Outer_Syntax.command (name, pos) descr
(ODL_Meta_Args_Parser.attributes -- Parse.document_source >> (fn (meta_args, text) =>
Toplevel.theory' (fn _ => cmd meta_args)
(Toplevel.presentation_context #> document_output_reports name mark meta_args text #> SOME)));
(Toplevel.presentation_context #> document_output_reports name mark transform_attr meta_args text #> SOME)));
(* Core Command Definitions *)
@ -2273,14 +2274,14 @@ val _ =
val _ =
document_command \<^command_keyword>\<open>text*\<close> "formal comment (primary style)"
{markdown = true, body = true} (gen_enriched_document_cmd {inline=true} I I);
{markdown = true, body = true} (gen_enriched_document_cmd {inline=true} I I) (K(K I));
(* This is just a stub at present *)
val _ =
document_command \<^command_keyword>\<open>text-macro*\<close> "formal comment macro"
{markdown = true, body = true}
(gen_enriched_document_cmd {inline=false} (* declare as macro *) I I);
(gen_enriched_document_cmd {inline=false} (* declare as macro *) I I) (K(K I));
val (declare_reference_default_class, declare_reference_default_class_setup)