From 3faf3102ee67a939a5dba18031dccc4030c4552a Mon Sep 17 00:00:00 2001 From: bu Date: Fri, 21 Feb 2020 15:39:50 +0100 Subject: [PATCH] First version with some places where type_synonyms were used to identify doc_classes --- src/DOF/Isa_COL.thy | 7 +++ src/DOF/Isa_DOF.thy | 107 ++++++++++++++++++++++++++------------------ 2 files changed, 70 insertions(+), 44 deletions(-) diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy index c0c2dea..fbbbd82 100644 --- a/src/DOF/Isa_COL.thy +++ b/src/DOF/Isa_COL.thy @@ -42,6 +42,10 @@ doc_class figure = placement :: placement spawn_columns :: bool <= True +ML\(Symtab.defined (#docclass_tab(DOF_core.get_data_global @{theory}))) "side_by_side_figure"\ + + +print_doc_classes doc_class side_by_side_figure = figure + anchor :: "string" @@ -51,6 +55,8 @@ doc_class side_by_side_figure = figure + anchor2 :: "string" caption2 :: "string" +print_doc_classes + doc_class figure_group = (* trace :: "doc_class rexp list" <= "[]" automatically generated since monitor clause *) @@ -59,6 +65,7 @@ doc_class figure_group = by the current LaTeX style-file. *) accepts "\figure\\<^sup>+" +print_doc_classes (* dito the future table *) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index dd0de4f..915d68c 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -78,7 +78,7 @@ val docclass_markup = docref_markup_gen docclassN \ -section\String Utilities\ +section\ Utilities\ ML\ fun spy x y = (writeln (x ^ y); y) @@ -116,6 +116,12 @@ fun holstring_to_bstring ctxt (x:string) : bstring = val t = String.concat (map collapse (chopper (fn x => x = #"@") x)); in t |> Syntax.string_of_term ctxt o Syntax.parse_term ctxt end; +fun map_option _ NONE = NONE + |map_option f (SOME x) = SOME (f x); + +fun map_optional _ s NONE = s + |map_optional f _ (SOME x) = f x; + \ section\ A HomeGrown Document Type Management (the ''Model'') \ @@ -275,41 +281,54 @@ fun typ_to_cid (Type(s,[@{typ "unit"}])) = Long_Name.qualifier s |typ_to_cid _ = error("type is not an ontological type.") -fun read_cid ctxt cid = +fun parse_cid ctxt cid = +(* parses a type lexically/syntactically, checks abscence of type vars *) (case Syntax.parse_typ ctxt cid of - Type(tyname, _) => tyname + Type(tyname, []) => tyname | _ => error "illegal type-format for doc-class-name.") handle ERROR _ => "" (* ignore error *) -(* -fun read_cid ctxt cid = + + +fun read_cid ctxt "text" = default_cid (* text = default_cid *) + | read_cid ctxt cid = +(* parses a type syntactically, type-identification, checking as class id *) (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 + ty as Type(tyname, _) => let val res = typ_to_cid ty + val t = #docclass_tab(get_data ctxt) + in if Symtab.defined t res + then res + else error("type identifier not a class id:"^res) + end | _ => error "illegal type-format for doc-class-name.") - handle ERROR _ => "" (* ignore error *) -*) + handle ERROR _ => error("type identifier not a class id:"^cid) + +fun parse_cid_global thy cid = parse_cid (Proof_Context.init_global thy) cid 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) +fun is_defined_cid_global cid thy = +(* works with short and long names *) + let val t = #docclass_tab(get_data_global thy) in cid=default_cid orelse - Symtab.defined t (read_cid_global thy cid) + Symtab.defined t (parse_cid_global thy cid) end -fun is_defined_cid_global' cid_long thy = let val t = #docclass_tab(get_data_global thy) +fun is_defined_cid_global' cid_long thy = +(* works with long names only *) + let val t = #docclass_tab(get_data_global thy) in cid_long=default_cid orelse Symtab.defined t cid_long end -fun is_defined_cid_local cid ctxt = let val t = #docclass_tab(get_data ctxt) +fun is_defined_cid_local cid ctxt = +(* works with short and long names *) + let val t = #docclass_tab(get_data ctxt) in cid=default_cid orelse - Symtab.defined t (read_cid ctxt cid) + Symtab.defined t (parse_cid ctxt cid) end -fun is_defined_cid_local' cid_long ctxt = let val t = #docclass_tab(get_data ctxt) +fun is_defined_cid_local' cid_long ctxt = +(* works with long names only *) + let val t = #docclass_tab(get_data ctxt) in cid_long=default_cid orelse Symtab.defined t cid_long end @@ -388,32 +407,29 @@ fun check_reject_atom cid_long term = fun define_doc_class_global (params', binding) parent fields rexp reject_Atoms thy = +(* This operation is executed in a context where the record has amready been defined, but + its conversion into a class is not yet done. *) let val nn = Context.theory_name thy (* in case that we need the thy-name to identify the space where it is ... *) val cid = (Binding.name_of binding) val pos = (Binding.pos_of binding) val _ = if is_defined_cid_global cid thy - then error("redefinition of document class") + then error("redefinition of document class:"^cid ) else () - - val _ = case parent of (* the doc_class may be root, but must refer - to another doc_class and not just an - arbitrary type *) - NONE => () - | SOME(_,cid_parent) => - if not (is_defined_cid_global cid_parent thy) - then error("document class undefined : " ^ cid_parent) - else () + val _ = map_option ((read_cid_global thy) o snd) parent + + (* weird construction. TODO replace by some read version *) val _ = writeln ("X::"^cid) - val cid_long = read_cid_global thy cid + val cid_long = parse_cid_global thy cid val _ = writeln ("Y::"^cid_long) - val cid_long' = read_cid_global thy cid_long + val cid_long' = parse_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); @@ -495,14 +511,14 @@ fun get_doc_class_local cid ctxt = fun is_defined_cid_local cid ctxt = let val t = #docclass_tab(get_data ctxt) in cid=default_cid orelse - Symtab.defined t (read_cid ctxt cid) + Symtab.defined t (parse_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 = read_cid ctxt cid (* to assure that the given cid is really a long_cid *) + val cid_long = parse_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 class id for attributes :"^cid) | SOME ({inherits_from=NONE, @@ -1019,9 +1035,16 @@ fun cid_2_cidType cid_long thy = fun base_default_term thy cid_long = Const(@{const_name "undefined"},cid_2_cidType thy cid_long) 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.read_cid_global thy cid + let + (* + val _ = if not (DOF_core.is_defined_cid_global cid thy) + then error("document class undefined") else () *) + val cid_long' = DOF_core.parse_cid_global thy cid + + + val cid_long = DOF_core.read_cid_global thy cid + val _ = writeln ("check_classref ::"^cid_long^"::"^cid_long') + 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!") @@ -1204,7 +1227,7 @@ fun gen_enriched_document_command transform (* as side-effect, generates markup *) fun check_text thy = (Pure_Syn_Ext.output_document(Toplevel.theory_toplevel thy) markdown toks; thy) - (* generating the level-attribute syntax *) + (* ... generating the level-attribute syntax *) in (create_and_check_docitem false oid pos cid_pos (transform doc_attrs) #> check_text) (* Thanks Frederic Tuong! ! ! *) @@ -1411,7 +1434,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.read_cid_global thy cid + | SOME(cid,_) => DOF_core.parse_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) @@ -1756,8 +1779,6 @@ fun read_parent NONE ctxt = (NONE, ctxt) Type (name, Ts) => (SOME (Ts, name), fold Variable.declare_typ Ts ctxt) | T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T)); -fun map_option _ NONE = NONE - |map_option f (SOME x) = SOME (f x); @@ -1795,11 +1816,9 @@ 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.read_cid_global thy (Binding.name_of binding) + fun cid thy = DOF_core.parse_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 - | SOME(_,str) => str + val parent_cid_long = map_optional snd DOF_core.default_cid parent; val raw_fieldsNdefaults' = filter (fn((bi,_,_),_) => Binding.name_of bi <> "trace") raw_fieldsNdefaults val _ = if length raw_fieldsNdefaults' <> length raw_fieldsNdefaults