diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy index 0f871b2..0e2b65a 100644 --- a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy @@ -2077,36 +2077,35 @@ space_implode "sd &e sf dfg" ["qs","er","alpa"]; text\Here is an abstract of the main interface to @{ML_structure Thy_Output}:\ -ML\ - output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text list; - output_token: Proof.context -> Token.T -> Latex.text list; - output_source: Proof.context -> string -> Latex.text list; - present_thy: Options.T -> theory -> segment list -> Latex.text list; +ML\ + Thy_Output.output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text list; + Thy_Output.output_token: Proof.context -> Token.T -> Latex.text list; + Thy_Output.output_source: Proof.context -> string -> Latex.text list; + Thy_Output.present_thy: Options.T -> theory -> Thy_Output.segment list -> Latex.text list; - isabelle: Proof.context -> Latex.text list -> Latex.text; + Thy_Output.isabelle: Proof.context -> Latex.text list -> Latex.text; - isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text; + Thy_Output.isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text; - typewriter: Proof.context -> string -> Latex.text; + Thy_Output.typewriter: Proof.context -> string -> Latex.text; - verbatim: Proof.context -> string -> Latex.text; + Thy_Output.verbatim: Proof.context -> string -> Latex.text; - source: Proof.context -> {embedded: bool} -> Token.src -> Latex.text; - - pretty: Proof.context -> Pretty.T -> Latex.text; - pretty_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T -> Latex.text; - pretty_items: Proof.context -> Pretty.T list -> Latex.text; - pretty_items_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T list -> Latex.text; + Thy_Output.source: Proof.context -> {embedded: bool} -> Token.src -> Latex.text; + Thy_Output.pretty: Proof.context -> Pretty.T -> Latex.text; + Thy_Output.pretty_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T -> Latex.text; + Thy_Output.pretty_items: Proof.context -> Pretty.T list -> Latex.text; + Thy_Output.pretty_items_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T list -> Latex.text; (* finally a number of antiquotation registries : *) - antiquotation_pretty: - binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory; - antiquotation_pretty_source: - binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory; - antiquotation_raw: - binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory; - antiquotation_verbatim: - binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory; + Thy_Output.antiquotation_pretty: + binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory; + Thy_Output.antiquotation_pretty_source: + binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory; + Thy_Output.antiquotation_raw: + binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory; + Thy_Output.antiquotation_verbatim: + binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory; \ diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy index 508e507..c0c2dea 100644 --- a/src/DOF/Isa_COL.thy +++ b/src/DOF/Isa_COL.thy @@ -35,12 +35,14 @@ datatype placement = pl_h | (*here*) pl_hb (*here -> bottom*) + doc_class figure = relative_width :: "int" (* percent of textwidth *) src :: "string" placement :: placement spawn_columns :: bool <= True + doc_class side_by_side_figure = figure + anchor :: "string" caption :: "string" diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 9354119..dd0de4f 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -262,7 +262,9 @@ fun get_automatas ({automatas, ... } : open_monitor_info) = automatas for doc-class-names. Note, however, that doc-classes are currently implemented by non-polymorphic records only; this means that the extensible "_ext" versions of type names must be reduced to qualifier names only. The used Syntax.parse_typ - handling the identification does that already. *) + handling the identification does that already. + However, we use Syntax.read_typ in order to allow type-synonyms which requires + an appropriate adaption in read_cid.*) fun is_subclass (ctxt) s t = is_subclass0(#docclass_tab(get_data ctxt)) s t fun is_subclass_global thy s t = is_subclass0(#docclass_tab(get_data_global thy)) s t @@ -273,18 +275,29 @@ fun typ_to_cid (Type(s,[@{typ "unit"}])) = Long_Name.qualifier s |typ_to_cid _ = error("type is not an ontological type.") -fun name2doc_class_name_local ctxt cid = +fun read_cid ctxt cid = (case Syntax.parse_typ ctxt cid of Type(tyname, _) => tyname - | _ => error "illegal format for doc-class-name.") + | _ => error "illegal type-format for doc-class-name.") handle ERROR _ => "" (* ignore error *) - -fun re_check_class_id thy cid = name2doc_class_name_local (Proof_Context.init_global thy) cid +(* +fun read_cid ctxt cid = + (case Syntax.read_typ ctxt cid of + Type(tyname, _) => let fun dropsuffix s n = String.substring (s, 0, size s - n) + in if String.isSuffix "_ext" tyname + then (* dropsuffix tyname 4 *) + Long_Name.qualifier tyname + else tyname + end + | _ => error "illegal type-format for doc-class-name.") + handle ERROR _ => "" (* ignore error *) +*) +fun read_cid_global thy cid = read_cid (Proof_Context.init_global thy) cid fun is_defined_cid_global cid thy = let val t = #docclass_tab(get_data_global thy) in cid=default_cid orelse - Symtab.defined t (re_check_class_id thy cid) + Symtab.defined t (read_cid_global thy cid) end fun is_defined_cid_global' cid_long thy = let val t = #docclass_tab(get_data_global thy) @@ -293,7 +306,7 @@ fun is_defined_cid_global' cid_long thy = let val t = #docclass_tab(get_data_glo fun is_defined_cid_local cid ctxt = let val t = #docclass_tab(get_data ctxt) in cid=default_cid orelse - Symtab.defined t (name2doc_class_name_local ctxt cid) + Symtab.defined t (read_cid ctxt cid) end fun is_defined_cid_local' cid_long ctxt = let val t = #docclass_tab(get_data ctxt) @@ -392,9 +405,15 @@ fun define_doc_class_global (params', binding) parent fields rexp reject_Atoms t if not (is_defined_cid_global cid_parent thy) then error("document class undefined : " ^ cid_parent) else () - val cid_long = re_check_class_id thy cid - val _ = if re_check_class_id thy cid_long <> "" then () - else error"Could not construct type from doc_class (lexical problem?)" + + val _ = writeln ("X::"^cid) + val cid_long = read_cid_global thy cid + val _ = writeln ("Y::"^cid_long) + val cid_long' = read_cid_global thy cid_long + val _ = writeln ("Z::"^cid_long') + val _ = writeln ("define_doc_class::" ^ cid_long ^"::"^ cid_long') + val _ = if cid_long' <> "" then () + else error("Could not construct type from doc_class (lexical problem?)") val id = serial (); val _ = Position.report pos (docclass_markup true cid id pos); @@ -437,14 +456,14 @@ fun define_object_local (oid, bbb) ctxt = (* declares an anonyme label of a given type and generates a unique reference ... *) fun declare_anoobject_global thy cid = let fun declare {tab,maxano} = let val str = cid^":"^Int.toString(maxano+1) - val _ = writeln("Anonymous doc-ref declared: " ^ str) + val _ = writeln("Anonymous reference declared: " ^ str) in {tab=Symtab.update(str,NONE)tab,maxano= maxano+1} end in map_data_global (upd_docobj_tab declare) (thy) end fun declare_anoobject_local ctxt cid = let fun declare {tab,maxano} = let val str = cid^":"^Int.toString(maxano+1) - val _ = writeln("Anonymous doc-ref declared: " ^str) + val _ = writeln("Anonymous reference declared: " ^str) in {tab=Symtab.update(str,NONE)tab, maxano=maxano+1} end in map_data (upd_docobj_tab declare) (ctxt) end @@ -463,30 +482,29 @@ fun get_object_local oid ctxt = case get_object_local_opt oid ctxt of |SOME(bbb) => bbb fun get_doc_class_global cid thy = - if cid = default_cid then error("default doc class acces") (* TODO *) + if cid = default_cid then error("default class acces") (* TODO *) else let val t = #docclass_tab(get_data_global thy) in (Symtab.lookup t cid) end fun get_doc_class_local cid ctxt = - if cid = default_cid then error("default doc class acces") (* TODO *) + if cid = default_cid then error("default class acces") (* TODO *) else let val t = #docclass_tab(get_data ctxt) in (Symtab.lookup t cid) end fun is_defined_cid_local cid ctxt = let val t = #docclass_tab(get_data ctxt) in cid=default_cid orelse - Symtab.defined t (name2doc_class_name_local ctxt cid) + Symtab.defined t (read_cid ctxt cid) end fun get_attributes_local cid ctxt = if cid = default_cid then [] else let val t = #docclass_tab(get_data ctxt) - val cid_long = name2doc_class_name_local ctxt cid (* to assure that the given cid is - really a long_cid *) + val cid_long = read_cid ctxt cid (* to assure that the given cid is really a long_cid *) in case Symtab.lookup t cid_long of - NONE => error("undefined doc class id for attributes :"^cid) + NONE => error("undefined class id for attributes :"^cid) | SOME ({inherits_from=NONE, attribute_decl = X, ...}) => [(cid_long,X)] | SOME ({inherits_from=SOME(_,father), @@ -867,13 +885,6 @@ setup\DOF_core.update_isa_global("docitem" ,ISA_core.ML_isa_check_docitem section\ Syntax for Annotated Documentation Commands (the '' View'' Part I) \ -ML\open Thy_Output; - -(*Pure_Syn.output_document;*) -Pure_Syn.document_command; -\ - -text\dfg\ (* text maps to Pure_Syn.document_command; *) (* ================== 2018 ====================================================== @@ -994,7 +1005,11 @@ fun cid_2_cidType cid_long thy = else let val t = #docclass_tab(DOF_core.get_data_global thy) fun ty_name cid = cid^"."^ Long_Name.base_name cid^"_ext" fun fathers cid_long = case Symtab.lookup t cid_long of - NONE => error("undefined doc class id :"^cid_long) + NONE => let val ctxt = Proof_Context.init_global thy + val tty = Syntax.parse_typ (Proof_Context.init_global thy) cid_long + val _ = writeln ("XXX"^(Syntax.string_of_typ ctxt tty)) + in error("undefined doc class id :"^cid_long) + end | SOME ({inherits_from=NONE, ...}) => [cid_long] | SOME ({inherits_from=SOME(_,father), ...}) => cid_long :: (fathers father) @@ -1006,7 +1021,7 @@ fun base_default_term thy cid_long = Const(@{const_name "undefined"},cid_2_cidTy fun check_classref is_monitor (SOME(cid,pos')) thy = let val _ = if not (DOF_core.is_defined_cid_global cid thy) then error("document class undefined") else () - val cid_long = DOF_core.re_check_class_id thy cid + val cid_long = DOF_core.read_cid_global thy cid val {id, name=bind_target,rex,...} = the(DOF_core.get_doc_class_global cid_long thy) val _ = if is_monitor andalso (null rex orelse cid_long= DOF_core.default_cid ) then error("should be monitor class!") @@ -1396,7 +1411,7 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : ODL_Command_Parse let val l = "label = "^ (enclose "{" "}" lab) val cid_long = case cid_opt of NONE => DOF_core.default_cid - | SOME(cid,_) => DOF_core.re_check_class_id thy cid + | SOME(cid,_) => DOF_core.read_cid_global thy cid val cid_txt = "type = " ^ (enclose "{" "}" cid_long); fun ltx_of_term _ _ (Const ("List.list.Cons", @{typ "char \ char list \ char list"}) $ t1 $ t2) @@ -1780,7 +1795,7 @@ fun add_doc_class_cmd overloaded (raw_params, binding) val ctxt = Proof_Context.init_global thy; val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params; val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt; - fun cid thy = DOF_core.re_check_class_id thy (Binding.name_of binding) + fun cid thy = DOF_core.read_cid_global thy (Binding.name_of binding) val (parent, ctxt2) = read_parent raw_parent ctxt1; val parent_cid_long = case parent of NONE => DOF_core.default_cid @@ -1872,4 +1887,10 @@ ML\open Goal\ ML \future_result;\ *) +ML\ String.isSuffix "_asd" "sdfgsd_asd"; + +String.substring ("sdfgsd_asd", 0, size "sdfgsd_asd" - 4)\ +ML\Long_Name.qualifier "dgfdfg.dfgdfg.qwe"\ + + end diff --git a/src/ontologies/CENELEC_50128/CENELEC_50128.thy b/src/ontologies/CENELEC_50128/CENELEC_50128.thy index dfae94a..f1ed167 100644 --- a/src/ontologies/CENELEC_50128/CENELEC_50128.thy +++ b/src/ontologies/CENELEC_50128/CENELEC_50128.thy @@ -708,8 +708,8 @@ section\ META : Testing and Validation \ text\Test : @{concept \COTS\}\ ML\ -DOF_core.re_check_class_id @{theory} "requirement"; -DOF_core.re_check_class_id @{theory} "SRAC"; +DOF_core.read_cid_global @{theory} "requirement"; +DOF_core.read_cid_global @{theory} "SRAC"; DOF_core.is_defined_cid_global "SRAC" @{theory}; DOF_core.is_defined_cid_global "EC" @{theory}; \ @@ -731,7 +731,7 @@ val internal_data_of_SRAC_definition = DOF_core.get_attributes_local "SRAC" @{co \ ML\ -DOF_core.re_check_class_id @{theory} "requirement"; +DOF_core.read_cid_global @{theory} "requirement"; Syntax.parse_typ @{context} "requirement"; val Type(t,_) = Syntax.parse_typ @{context} "requirement" handle ERROR _ => dummyT; Syntax.read_typ @{context} "hypothesis" handle _ => dummyT; diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index 718de0f..4a219ef 100644 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -77,20 +77,26 @@ doc_class technical = text_section + definition_list :: "string list" <= "[]" status :: status <= "description" formal_results :: "thm list" + +type_synonym tc = technical text\A rough structuring is modeled as follows:\ doc_class "definition" = technical + + referentiable :: bool <= "True" tag :: "string" <= "''''" doc_class "theorem" = technical + + referentiable :: bool <= "True" tag :: "string" <= "''''" text\Note that the following two text-elements are currently set to no-keyword in LNCS style.\ doc_class "lemma" = technical + + referentiable :: bool <= "True" tag :: "string" <= "''''" doc_class "corollary" = technical + + referentiable :: bool <= "True" tag :: "string" <= "''''" @@ -98,9 +104,11 @@ text\ \<^verbatim>\examples\ are currently considered \<^verb following classes into an own class: "evaluation" or "explanation" or ... \ doc_class example = technical + + referentiable :: bool <= "True" tag :: "string" <= "''''" doc_class assertion = technical + + referentiable :: bool <= "True" tag :: "string" <= "''''"