2018-03-28 07:24:27 +00:00
|
|
|
chapter \<open>The Document-Type Support Framework for Isabelle\<close>
|
2018-02-07 18:44:27 +00:00
|
|
|
|
|
|
|
text{* Offering reflection to ML for class hierarchies, objects and object states.
|
|
|
|
+ Isar syntax for these, assuming that classes entities fit to predefined
|
|
|
|
Isar keywords.
|
|
|
|
*}
|
|
|
|
|
|
|
|
text{* In this section, we develop on the basis of a management of references Isar-markups
|
|
|
|
that provide direct support in the PIDE framework. *}
|
|
|
|
|
|
|
|
theory Isa_DOF (* Isabelle Document Ontology Framework *)
|
2018-03-28 07:24:27 +00:00
|
|
|
imports Main (* Isa_MOF *)
|
2018-02-07 18:44:27 +00:00
|
|
|
keywords "section*" "subsection*" "subsubsection*"
|
|
|
|
"paragraph*" "subparagraph*" "text*" "declare_reference"::thy_decl
|
|
|
|
and
|
|
|
|
"doc_class" :: thy_decl
|
|
|
|
|
|
|
|
begin
|
|
|
|
|
|
|
|
|
|
|
|
section{* A HomeGrown Document Type Management (the ''Model'') *}
|
|
|
|
|
|
|
|
ML{*
|
|
|
|
curry;
|
|
|
|
op |>;
|
|
|
|
op #>;
|
|
|
|
op |>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c;
|
2018-02-09 11:25:15 +00:00
|
|
|
op ||> : ('c * 'a) * ('a -> 'b) -> 'c * 'b;
|
2018-02-28 13:06:52 +00:00
|
|
|
|
|
|
|
val docrefN = "docref";
|
|
|
|
|
|
|
|
(* derived from: theory_markup *)
|
|
|
|
fun docref_markup def name id pos =
|
|
|
|
if id = 0 then Markup.empty
|
|
|
|
else
|
|
|
|
Markup.properties (Position.entity_properties_of def id pos)
|
|
|
|
(Markup.entity docrefN name); (* or better store the thy-name as property ? ? ? *)
|
|
|
|
|
2018-02-07 18:44:27 +00:00
|
|
|
*}
|
|
|
|
|
2018-02-08 15:25:15 +00:00
|
|
|
|
2018-02-07 18:44:27 +00:00
|
|
|
|
|
|
|
ML{*
|
|
|
|
|
2018-02-09 11:25:15 +00:00
|
|
|
structure DOF_core =
|
2018-02-07 18:44:27 +00:00
|
|
|
struct
|
2018-02-08 15:25:15 +00:00
|
|
|
type docclass_struct = {params : (string * sort) list, (*currently not used *)
|
|
|
|
name : binding, thy_name : string, id : serial, (* for pide *)
|
|
|
|
inherits_from : (typ list * string) option,
|
|
|
|
attribute_decl : (binding * typ * term option) list
|
|
|
|
(*, rex : term list -- not yet used *)}
|
|
|
|
|
2018-02-07 18:44:27 +00:00
|
|
|
|
|
|
|
type docclass_tab = docclass_struct Symtab.table
|
|
|
|
|
|
|
|
val initial_docclass_tab = Symtab.empty:docclass_tab
|
|
|
|
|
|
|
|
fun merge_docclass_tab (otab,otab') = Symtab.merge (op =) (otab,otab')
|
|
|
|
|
2018-02-28 10:31:42 +00:00
|
|
|
|
2018-02-28 13:06:52 +00:00
|
|
|
val default_cid = "text" (* the top (default) document class: everything is a text.*)
|
2018-02-28 10:31:42 +00:00
|
|
|
|
|
|
|
fun is_subclass0 (tab:docclass_tab) s t =
|
2018-02-07 18:44:27 +00:00
|
|
|
let val _ = case Symtab.lookup tab t of
|
2018-02-28 10:31:42 +00:00
|
|
|
NONE => if t <> default_cid
|
|
|
|
then error "document superclass not defined"
|
|
|
|
else default_cid
|
|
|
|
| SOME _ => ""
|
2018-02-07 18:44:27 +00:00
|
|
|
fun father_is_sub s = case Symtab.lookup tab s of
|
2018-02-28 10:31:42 +00:00
|
|
|
NONE => error "document subclass not defined"
|
2018-02-08 15:25:15 +00:00
|
|
|
| SOME ({inherits_from=NONE, ...}) => s = t
|
2018-02-28 10:31:42 +00:00
|
|
|
| SOME ({inherits_from=SOME (_,s'), ...}) =>
|
|
|
|
s' = t orelse father_is_sub s'
|
|
|
|
in s = t orelse
|
|
|
|
(t = default_cid andalso Symtab.defined tab s ) orelse
|
|
|
|
father_is_sub s
|
2018-02-07 18:44:27 +00:00
|
|
|
end
|
|
|
|
|
|
|
|
type docobj = {pos : Position.T, thy_name : string, id : serial, cid : string}
|
|
|
|
|
|
|
|
type docobj_tab ={tab : (docobj option) Symtab.table,
|
|
|
|
maxano : int
|
|
|
|
}
|
|
|
|
|
|
|
|
val initial_docobj_tab:docobj_tab = {tab = Symtab.empty, maxano = 0}
|
|
|
|
|
|
|
|
fun merge_docobj_tab ({tab=otab,maxano=m}, {tab=otab',maxano=m'}) =
|
|
|
|
(let fun X(NONE,NONE) = false
|
|
|
|
|X(SOME _, NONE) = false
|
|
|
|
|X(NONE, SOME _) = false
|
|
|
|
|X(SOME b, SOME b') = true (* b = b' *)
|
|
|
|
in {tab=Symtab.merge X (otab,otab'),maxano=Int.max(m,m')}
|
|
|
|
end)
|
|
|
|
|
|
|
|
|
|
|
|
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))
|
|
|
|
);
|
|
|
|
|
|
|
|
val get_data = Data.get o Context.Proof;
|
|
|
|
val map_data = Data.map;
|
|
|
|
val get_data_global = Data.get o Context.Theory;
|
|
|
|
val map_data_global = Context.theory_map o map_data;
|
|
|
|
|
2018-02-27 11:02:19 +00:00
|
|
|
|
|
|
|
(* doc-class-name management: We still use the record-package for internally
|
|
|
|
representing doc-classes. The main motivation is that "links" to entities are
|
|
|
|
types over doc-classes, *types* in the Isabelle sense, enriched by additional data.
|
|
|
|
This has the advantage that the type-inference can be abused to infer long-names
|
|
|
|
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. *)
|
|
|
|
|
2018-02-28 10:31:42 +00:00
|
|
|
fun is_subclass (ctxt) s t = is_subclass0(snd(get_data ctxt)) s t
|
|
|
|
|
2018-02-27 11:02:19 +00:00
|
|
|
fun type_name2doc_class_name thy str = (* Long_Name.qualifier *) str
|
|
|
|
|
|
|
|
fun name2doc_class_name thy str =
|
|
|
|
case Syntax.parse_typ (Proof_Context.init_global thy) str of
|
|
|
|
Type(tyn, _) => type_name2doc_class_name thy tyn
|
|
|
|
| _ => error "illegal format for doc-class-name."
|
|
|
|
handle ERROR _ => ""
|
|
|
|
|
|
|
|
fun name2doc_class_name_local ctxt str =
|
|
|
|
(case Syntax.parse_typ ctxt str of
|
|
|
|
Type(tyn, _) => type_name2doc_class_name ctxt tyn
|
|
|
|
| _ => error "illegal format for doc-class-name.")
|
|
|
|
handle ERROR _ => ""
|
|
|
|
|
|
|
|
|
2018-02-08 15:25:15 +00:00
|
|
|
|
|
|
|
fun is_defined_cid_global cid thy = let val t = snd(get_data_global thy)
|
2018-02-27 11:02:19 +00:00
|
|
|
in cid=default_cid orelse
|
|
|
|
Symtab.defined t (name2doc_class_name thy cid)
|
|
|
|
end
|
|
|
|
|
2018-02-08 15:25:15 +00:00
|
|
|
|
|
|
|
fun is_defined_cid_local cid ctxt = let val t = snd(get_data ctxt)
|
2018-02-27 11:02:19 +00:00
|
|
|
in cid=default_cid orelse
|
|
|
|
Symtab.defined t (name2doc_class_name_local ctxt cid)
|
|
|
|
end
|
2018-02-08 15:25:15 +00:00
|
|
|
|
2018-02-07 18:44:27 +00:00
|
|
|
|
|
|
|
fun is_declared_oid_global oid thy = let val {tab=t,maxano=_} = fst(get_data_global thy)
|
|
|
|
in Symtab.defined t oid end
|
|
|
|
|
|
|
|
fun is_declared_oid_local oid thy = let val {tab=t,maxano=_} = fst(get_data thy)
|
|
|
|
in Symtab.defined t oid end
|
|
|
|
|
|
|
|
fun is_defined_oid_global oid thy = let val {tab=t,maxano=_} = fst(get_data_global thy)
|
|
|
|
in case Symtab.lookup t oid of
|
|
|
|
NONE => false
|
|
|
|
|SOME(NONE) => false
|
|
|
|
|SOME _ => true
|
|
|
|
end
|
|
|
|
|
|
|
|
fun is_defined_oid_local oid thy = let val {tab=t,maxano=_} = fst(get_data thy)
|
|
|
|
in case Symtab.lookup t oid of
|
|
|
|
NONE => false
|
|
|
|
|SOME(NONE) => false
|
|
|
|
|SOME _ => true
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
|
|
fun declare_object_global oid thy = (map_data_global
|
2018-02-08 15:25:15 +00:00
|
|
|
(apfst(fn {tab=t,maxano=x} =>
|
|
|
|
{tab=Symtab.update_new(oid,NONE)t,
|
|
|
|
maxano=x}))
|
2018-02-07 18:44:27 +00:00
|
|
|
(thy)
|
|
|
|
handle Symtab.DUP _ =>
|
|
|
|
error("multiple declaration of document reference"))
|
|
|
|
|
2018-02-08 15:25:15 +00:00
|
|
|
fun declare_object_local oid ctxt = (map_data (apfst(fn {tab=t,maxano=x} =>
|
|
|
|
{tab=Symtab.update_new(oid,NONE) t,
|
|
|
|
maxano=x}))
|
2018-02-07 18:44:27 +00:00
|
|
|
(ctxt)
|
|
|
|
handle Symtab.DUP _ =>
|
|
|
|
error("multiple declaration of document reference"))
|
|
|
|
|
2018-02-28 13:06:52 +00:00
|
|
|
|
2018-02-08 15:25:15 +00:00
|
|
|
fun define_doc_class_global (params', binding) parent fields thy =
|
|
|
|
let val nn = Context.theory_name thy (* in case that we need the thy-name to identify
|
|
|
|
the space where it is ... *)
|
2018-02-27 11:02:19 +00:00
|
|
|
val cid = (Binding.name_of binding)
|
2018-02-28 13:06:52 +00:00
|
|
|
val pos = (Binding.pos_of binding)
|
2018-02-27 11:02:19 +00:00
|
|
|
|
|
|
|
val _ = if is_defined_cid_global cid thy
|
|
|
|
then error("redefinition of document class")
|
2018-02-09 11:25:15 +00:00
|
|
|
else ()
|
2018-02-27 11:02:19 +00:00
|
|
|
|
2018-02-09 11:25:15 +00:00
|
|
|
val _ = case parent of (* the doc_class may be root, but must refer
|
|
|
|
to another doc_class and not just an
|
|
|
|
arbitrary type *)
|
|
|
|
NONE => ()
|
2018-02-28 10:31:42 +00:00
|
|
|
| SOME(_,cid_parent) =>
|
|
|
|
if not (is_defined_cid_global cid_parent thy)
|
|
|
|
then error("document class undefined : " ^ cid_parent)
|
|
|
|
else ()
|
2018-02-27 11:02:19 +00:00
|
|
|
val cid_long = name2doc_class_name thy cid
|
2018-02-28 13:06:52 +00:00
|
|
|
val id = serial ();
|
|
|
|
val _ = Position.report pos (docref_markup true cid id pos);
|
|
|
|
|
2018-02-27 11:02:19 +00:00
|
|
|
val info = {params=params',
|
2018-02-08 15:25:15 +00:00
|
|
|
name = binding,
|
|
|
|
thy_name = nn,
|
2018-02-28 13:06:52 +00:00
|
|
|
id = id, (* for pide --- really fresh or better reconstruct
|
2018-02-08 15:25:15 +00:00
|
|
|
from prior record definition ? *)
|
|
|
|
inherits_from = parent,
|
|
|
|
attribute_decl = fields (* currently unchecked *)
|
|
|
|
(*, rex : term list -- not yet used *)}
|
2018-02-28 13:06:52 +00:00
|
|
|
val _ = () (* XXX *)
|
|
|
|
|
2018-02-27 11:02:19 +00:00
|
|
|
in map_data_global(apsnd(Symtab.update(cid_long,info)))(thy)
|
2018-02-08 15:25:15 +00:00
|
|
|
end
|
|
|
|
|
2018-02-07 18:44:27 +00:00
|
|
|
|
|
|
|
fun define_object_global (oid, bbb) thy =
|
|
|
|
let val nn = Context.theory_name thy (* in case that we need the thy-name to identify
|
|
|
|
the space where it is ... *)
|
|
|
|
in if is_defined_oid_global oid thy
|
|
|
|
then error("multiple definition of document reference")
|
2018-02-08 15:25:15 +00:00
|
|
|
else map_data_global (apfst(fn {tab=t,maxano=x} =>
|
|
|
|
{tab=Symtab.update(oid,SOME bbb) t,
|
|
|
|
maxano=x}))
|
2018-02-07 18:44:27 +00:00
|
|
|
(thy)
|
|
|
|
end
|
|
|
|
|
|
|
|
fun define_object_local (oid, bbb) ctxt =
|
2018-02-08 15:25:15 +00:00
|
|
|
map_data (apfst(fn {tab=t,maxano=x} =>
|
|
|
|
{tab=Symtab.update(oid,SOME bbb) t,maxano=x})) ctxt
|
2018-02-07 18:44:27 +00:00
|
|
|
|
|
|
|
|
|
|
|
(* declares an anonyme label of a given type and generates a unique reference ... *)
|
|
|
|
fun declare_anoobject_global thy cid = map_data_global
|
2018-02-08 15:25:15 +00:00
|
|
|
(apfst(fn {tab=t,maxano=x} =>
|
|
|
|
let val str = cid^":"^Int.toString(x+1)
|
|
|
|
val _ = writeln("Anonymous doc-ref declared: "
|
|
|
|
^str)
|
|
|
|
in {tab=Symtab.update(str,NONE)t,maxano=x+1}
|
|
|
|
end))
|
2018-02-07 18:44:27 +00:00
|
|
|
(thy)
|
|
|
|
|
|
|
|
fun declare_anoobject_local ctxt cid = map_data
|
2018-02-08 15:25:15 +00:00
|
|
|
(apfst(fn {tab=t,maxano=x} =>
|
|
|
|
let val str = cid^":"^Int.toString(x+1)
|
|
|
|
val _ = writeln("Anonymous doc-ref declared: "
|
2018-02-07 18:44:27 +00:00
|
|
|
^str)
|
2018-02-08 15:25:15 +00:00
|
|
|
in {tab=Symtab.update(str,NONE)t, maxano=x+1}
|
|
|
|
end))
|
2018-02-07 18:44:27 +00:00
|
|
|
(ctxt)
|
|
|
|
|
2018-02-28 10:31:42 +00:00
|
|
|
|
2018-02-07 18:44:27 +00:00
|
|
|
fun get_object_global oid thy = let val {tab=t,maxano=_} = fst(get_data_global thy)
|
|
|
|
in case Symtab.lookup t oid of
|
|
|
|
NONE => error"undefined reference"
|
|
|
|
|SOME(bbb) => bbb
|
|
|
|
end
|
|
|
|
|
|
|
|
fun get_object_local oid ctxt = let val {tab=t,maxano=_} = fst(get_data ctxt)
|
|
|
|
in case Symtab.lookup t oid of
|
|
|
|
NONE => error"undefined reference"
|
|
|
|
|SOME(bbb) => bbb
|
|
|
|
end
|
|
|
|
|
2018-02-28 10:31:42 +00:00
|
|
|
fun get_doc_class_global cid thy =
|
|
|
|
if cid = default_cid then error("default doc class acces") (* TODO *)
|
|
|
|
else let val t = snd(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 *)
|
|
|
|
else let val t = snd(get_data ctxt)
|
|
|
|
in (Symtab.lookup t cid) end
|
|
|
|
|
|
|
|
|
|
|
|
fun is_defined_cid_local cid ctxt = let val t = snd(get_data ctxt)
|
|
|
|
in cid=default_cid orelse
|
|
|
|
Symtab.defined t (name2doc_class_name_local ctxt cid)
|
|
|
|
end
|
|
|
|
|
2018-02-28 13:06:52 +00:00
|
|
|
fun writeln_classrefs ctxt = let val t = snd(get_data ctxt)
|
|
|
|
in writeln (String.concatWith "," (Symtab.keys t)) end
|
|
|
|
|
2018-02-07 18:44:27 +00:00
|
|
|
|
2018-02-28 13:06:52 +00:00
|
|
|
fun writeln_docrefs ctxt = let val {tab=t,maxano=_} = fst(get_data ctxt)
|
2018-02-07 18:44:27 +00:00
|
|
|
in writeln (String.concatWith "," (Symtab.keys t)) end
|
|
|
|
end (* struct *)
|
|
|
|
*}
|
|
|
|
|
|
|
|
|
|
|
|
section{* Syntax for Annotated Documentation Commands (the '' View'') *}
|
|
|
|
|
|
|
|
|
|
|
|
ML{*
|
|
|
|
structure DocAttrParser =
|
|
|
|
struct
|
|
|
|
|
|
|
|
val semi = Scan.option (Parse.$$$ ";");
|
|
|
|
|
|
|
|
val attribute =
|
2018-02-08 15:25:15 +00:00
|
|
|
Parse.position Parse.name
|
|
|
|
-- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) "";
|
2018-02-07 18:44:27 +00:00
|
|
|
|
2018-02-28 10:31:42 +00:00
|
|
|
|
2018-02-07 18:44:27 +00:00
|
|
|
val reference =
|
2018-02-08 15:25:15 +00:00
|
|
|
Parse.position Parse.name
|
2018-02-28 10:31:42 +00:00
|
|
|
-- Scan.option (Parse.$$$ "::" |-- Parse.!!! (Parse.position Parse.name));
|
|
|
|
|
2018-02-07 18:44:27 +00:00
|
|
|
|
|
|
|
val attributes = (Parse.$$$ "[" |-- (reference --
|
|
|
|
(Scan.optional(Parse.$$$ "," |-- (Parse.enum "," attribute))) []))
|
|
|
|
--| Parse.$$$ "]"
|
|
|
|
|
|
|
|
|
2018-02-28 10:31:42 +00:00
|
|
|
fun enriched_document_command markdown (((((oid,pos),cid_pos),doc_attrs),
|
2018-02-07 18:44:27 +00:00
|
|
|
xstring_opt:(xstring * Position.T) option),
|
2018-02-28 13:06:52 +00:00
|
|
|
toks:Input.source) =
|
2018-02-07 18:44:27 +00:00
|
|
|
let
|
|
|
|
val id = serial ();
|
|
|
|
val _ = Position.report pos (docref_markup true oid id pos);
|
|
|
|
(* creates a markup label for this position and reports it to the PIDE framework;
|
|
|
|
this label is used as jump-target for point-and-click feature. *)
|
2018-02-28 10:31:42 +00:00
|
|
|
|
|
|
|
fun enrich_trans (SOME(cid,pos')) thy =
|
|
|
|
let val name = Context.theory_name thy
|
2018-02-09 11:25:15 +00:00
|
|
|
val _ = if not (DOF_core.is_defined_cid_global cid thy)
|
2018-02-28 10:31:42 +00:00
|
|
|
then error("document class undefined")
|
2018-02-08 15:25:15 +00:00
|
|
|
else ()
|
2018-02-28 10:31:42 +00:00
|
|
|
val cid_long = DOF_core.name2doc_class_name thy cid
|
|
|
|
val _ = writeln cid_long
|
2018-02-28 13:06:52 +00:00
|
|
|
|
|
|
|
(*
|
|
|
|
val {pos=pos_decl,id,cid,...} = the(DOF_core.get_object_global name thy)
|
|
|
|
val markup = docref_markup false name id pos_decl;
|
|
|
|
val _ = Context_Position.report ctxt pos markup;
|
|
|
|
Context.Theory;
|
|
|
|
Context_Position.report_generic;
|
|
|
|
|
|
|
|
*)
|
|
|
|
val {id, name=bind_target,...} =
|
|
|
|
the(DOF_core.get_doc_class_global cid_long thy)
|
|
|
|
val markup = docref_markup false cid id (Binding.pos_of bind_target);
|
|
|
|
val ctxt = Context.Theory thy
|
|
|
|
val _ = Context_Position.report_generic ctxt pos' markup;
|
|
|
|
|
|
|
|
|
2018-02-09 11:25:15 +00:00
|
|
|
in DOF_core.define_object_global (oid, {pos=pos, thy_name=name,
|
2018-02-28 10:31:42 +00:00
|
|
|
id=id, cid=cid_long})
|
2018-02-07 18:44:27 +00:00
|
|
|
(thy)
|
2018-02-28 10:31:42 +00:00
|
|
|
end
|
|
|
|
| enrich_trans NONE thy =
|
|
|
|
let val name = Context.theory_name thy
|
|
|
|
in DOF_core.define_object_global
|
|
|
|
(oid, {pos=pos, thy_name=name,
|
|
|
|
id=id , cid=DOF_core.default_cid})
|
|
|
|
(thy)
|
|
|
|
end
|
2018-02-07 18:44:27 +00:00
|
|
|
fun MMM(SOME(s,p)) = SOME(s^"XXX",p)
|
|
|
|
|MMM(NONE) = SOME("XXX",Position.id "")
|
|
|
|
in
|
2018-02-28 10:31:42 +00:00
|
|
|
(Toplevel.theory(enrich_trans cid_pos)) #>
|
2018-02-07 18:44:27 +00:00
|
|
|
(Thy_Output.document_command markdown (MMM xstring_opt,toks)) #>
|
|
|
|
(Thy_Output.document_command markdown (SOME("\\label{"^oid^"}", Position.id ""),toks)) #>
|
|
|
|
(Thy_Output.document_command markdown (SOME("\\label{"^oid^"}", Position.id ""),toks))
|
|
|
|
end;
|
|
|
|
|
|
|
|
|
|
|
|
val _ =
|
|
|
|
Outer_Syntax.command ("section*", @{here}) "section heading"
|
|
|
|
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
|
|
|
>> enriched_document_command {markdown = false});
|
|
|
|
|
|
|
|
val _ =
|
|
|
|
Outer_Syntax.command ("subsection*", @{here}) "subsection heading"
|
|
|
|
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
|
|
|
>> enriched_document_command {markdown = false});
|
|
|
|
|
|
|
|
val _ =
|
|
|
|
Outer_Syntax.command ("subsubsection*", @{here}) "subsubsection heading"
|
|
|
|
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
|
|
|
>> enriched_document_command {markdown = false});
|
|
|
|
|
|
|
|
val _ =
|
|
|
|
Outer_Syntax.command ("paragraph*", @{here}) "paragraph heading"
|
|
|
|
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
|
|
|
>> enriched_document_command {markdown = false});
|
|
|
|
|
|
|
|
val _ =
|
|
|
|
Outer_Syntax.command ("subparagraph*", @{here}) "subparagraph heading"
|
|
|
|
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
|
|
|
>> enriched_document_command {markdown = false});
|
|
|
|
|
|
|
|
val _ =
|
|
|
|
Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)"
|
|
|
|
(attributes -- Parse.opt_target -- Parse.document_source
|
|
|
|
>> enriched_document_command {markdown = false});
|
|
|
|
|
|
|
|
val _ =
|
|
|
|
Outer_Syntax.command @{command_keyword "declare_reference"} "declare document reference"
|
|
|
|
(attributes >> (fn (((oid,pos),cid),doc_attrs) =>
|
2018-02-09 11:25:15 +00:00
|
|
|
(Toplevel.theory (DOF_core.declare_object_global oid))));
|
2018-02-07 18:44:27 +00:00
|
|
|
|
|
|
|
|
|
|
|
(* Proof.context -> Symtab.key * Position.T -> Pretty.T ; dead code:
|
|
|
|
fun pretty_docref ctxt (name, pos) =
|
|
|
|
let
|
2018-02-09 11:25:15 +00:00
|
|
|
(* val _ = DOF_core.writeln_keys ctxt *)
|
2018-02-07 18:44:27 +00:00
|
|
|
val thy = Proof_Context.theory_of ctxt;
|
|
|
|
fun pretty_docref str = let val tok = Pretty.enclose "\\autoref{" "}" (Pretty.text (str))
|
|
|
|
(* val _ = writeln (Pretty.string_of tok) *)
|
|
|
|
in tok end
|
|
|
|
in
|
2018-02-09 11:25:15 +00:00
|
|
|
if DOF_core.is_defined_oid_global name thy
|
|
|
|
then let val {pos=pos_decl,id,...} = the(DOF_core.get_object_global name thy)
|
2018-02-07 18:44:27 +00:00
|
|
|
val markup = docref_markup false name id pos_decl;
|
|
|
|
val _ = Context_Position.report ctxt pos markup;
|
|
|
|
(* this sends a report to the PIDE interface ... *)
|
|
|
|
in pretty_docref name end
|
2018-02-09 11:25:15 +00:00
|
|
|
else if DOF_core.is_declared_oid_global name thy
|
2018-02-07 18:44:27 +00:00
|
|
|
then (warning("declared but undefined document reference:"^name);
|
|
|
|
pretty_docref name)
|
|
|
|
else error("undefined document reference:"^name)
|
|
|
|
end
|
|
|
|
*)
|
|
|
|
|
|
|
|
|
2018-02-28 10:31:42 +00:00
|
|
|
fun check_and_mark ctxt cid_decl (str:{strict_checking: bool}) pos name =
|
2018-02-07 18:44:27 +00:00
|
|
|
let
|
|
|
|
val thy = Proof_Context.theory_of ctxt;
|
|
|
|
in
|
2018-02-09 11:25:15 +00:00
|
|
|
if DOF_core.is_defined_oid_global name thy
|
2018-02-28 10:31:42 +00:00
|
|
|
then let val {pos=pos_decl,id,cid,...} = the(DOF_core.get_object_global name thy)
|
2018-02-07 18:44:27 +00:00
|
|
|
val markup = docref_markup false name id pos_decl;
|
|
|
|
val _ = Context_Position.report ctxt pos markup;
|
2018-02-28 13:06:52 +00:00
|
|
|
(* this sends a report for a ref application to the PIDE interface ... *)
|
|
|
|
val _ = if cid <> DOF_core.default_cid
|
|
|
|
andalso not(DOF_core.is_subclass ctxt cid cid_decl)
|
2018-02-28 10:31:42 +00:00
|
|
|
then error("reference ontologically inconsistent")
|
2018-02-28 13:06:52 +00:00
|
|
|
else ()
|
2018-02-07 18:44:27 +00:00
|
|
|
in name end
|
2018-02-09 11:25:15 +00:00
|
|
|
else if DOF_core.is_declared_oid_global name thy
|
2018-02-07 18:44:27 +00:00
|
|
|
then (if #strict_checking str then warning("declared but undefined document reference:"^name)
|
|
|
|
else (); name)
|
|
|
|
else error("undefined document reference:"^name)
|
|
|
|
end
|
|
|
|
|
|
|
|
(* superfluous :
|
|
|
|
fun basic_entities_style name scan pretty =
|
|
|
|
Thy_Output.antiquotation name scan (fn {source, context = ctxt, ...} => fn (style, xs) =>
|
|
|
|
Thy_Output.output ctxt
|
|
|
|
(Thy_Output.maybe_pretty_source (fn ctxt => fn x => pretty ctxt (style, x)) ctxt source xs));
|
|
|
|
|
|
|
|
fun basic_entities name scan pretty =
|
|
|
|
Thy_Output.antiquotation name scan (fn {source, context = ctxt, ...} =>
|
|
|
|
Thy_Output.output ctxt o Thy_Output.maybe_pretty_source pretty ctxt source);
|
|
|
|
|
|
|
|
fun basic_entity name scan = basic_entities name (scan >> single);
|
|
|
|
*)
|
|
|
|
|
2018-02-28 10:31:42 +00:00
|
|
|
fun control_antiquotation name cid_decl (str:{strict_checking: bool}) s1 s2 =
|
2018-02-07 18:44:27 +00:00
|
|
|
Thy_Output.antiquotation name (Scan.lift (Args.cartouche_input))
|
|
|
|
(fn {context =ctxt, source = src:Token.src, state} =>
|
|
|
|
fn source:Input.source =>
|
|
|
|
(Thy_Output.output_text state {markdown=false} #>
|
2018-02-28 10:31:42 +00:00
|
|
|
check_and_mark ctxt cid_decl (str:{strict_checking: bool})(Input.pos_of source) #>
|
2018-02-07 18:44:27 +00:00
|
|
|
enclose s1 s2)
|
|
|
|
source);
|
|
|
|
|
2018-02-28 13:06:52 +00:00
|
|
|
|
|
|
|
(* Setup for general docrefs of the global DOF_core.default_cid - class ("text")*)
|
2018-02-07 18:44:27 +00:00
|
|
|
val _ = Theory.setup
|
2018-02-28 10:31:42 +00:00
|
|
|
((control_antiquotation @{binding docref} DOF_core.default_cid {strict_checking=true} "\\autoref{" "}" ) #>
|
|
|
|
(control_antiquotation @{binding docref_unchecked} DOF_core.default_cid {strict_checking=false} "\\autoref{" "}")#>
|
|
|
|
(control_antiquotation @{binding docref_define} DOF_core.default_cid {strict_checking=false} "\\label{" "}"))
|
2018-02-07 18:44:27 +00:00
|
|
|
|
|
|
|
end (* struct *)
|
|
|
|
*}
|
|
|
|
|
|
|
|
ML{*
|
|
|
|
|
|
|
|
fun read_parent NONE ctxt = (NONE, ctxt)
|
|
|
|
| read_parent (SOME raw_T) ctxt =
|
|
|
|
(case Proof_Context.read_typ_abbrev ctxt raw_T of
|
|
|
|
Type (name, Ts) => (SOME (Ts, name), fold Variable.declare_typ Ts ctxt)
|
|
|
|
| T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T));
|
|
|
|
|
2018-02-08 15:25:15 +00:00
|
|
|
|
2018-02-27 11:02:19 +00:00
|
|
|
fun map_option _ NONE = NONE
|
2018-02-08 15:25:15 +00:00
|
|
|
|map_option f (SOME x) = SOME (f x)
|
|
|
|
|
2018-02-07 18:44:27 +00:00
|
|
|
fun read_fields raw_fields ctxt =
|
|
|
|
let
|
2018-02-08 15:25:15 +00:00
|
|
|
val Ts = Syntax.read_typs ctxt (map (fn ((_, raw_T, _),_) => raw_T) raw_fields);
|
|
|
|
val terms = map ((map_option (Syntax.read_term ctxt)) o snd) raw_fields
|
|
|
|
val fields = map2 (fn ((x, _, mx),_) => fn T => (x, T, mx)) raw_fields Ts;
|
2018-02-07 18:44:27 +00:00
|
|
|
val ctxt' = fold Variable.declare_typ Ts ctxt;
|
2018-02-08 15:25:15 +00:00
|
|
|
in (fields, terms, ctxt') end;
|
2018-02-07 18:44:27 +00:00
|
|
|
|
2018-02-27 11:02:19 +00:00
|
|
|
fun add_record_cmd overloaded (raw_params, binding) raw_parent raw_fieldsNdefaults _ thy =
|
2018-02-07 18:44:27 +00:00
|
|
|
let
|
|
|
|
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;
|
|
|
|
val (parent, ctxt2) = read_parent raw_parent ctxt1;
|
2018-02-08 15:25:15 +00:00
|
|
|
val (fields, terms, ctxt3) = read_fields raw_fieldsNdefaults ctxt2;
|
|
|
|
val fieldsNterms = (map (fn (a,b,_) => (a,b)) fields) ~~ terms
|
|
|
|
val fieldsNterms' = map (fn ((x,y),z) => (x,y,z)) fieldsNterms
|
2018-02-07 18:44:27 +00:00
|
|
|
val params' = map (Proof_Context.check_tfree ctxt3) params;
|
2018-02-08 15:25:15 +00:00
|
|
|
in thy |> Record.add_record overloaded (params', binding) parent fields
|
2018-02-09 11:25:15 +00:00
|
|
|
|> DOF_core.define_doc_class_global (params', binding) parent fieldsNterms'
|
2018-02-08 15:25:15 +00:00
|
|
|
end;
|
2018-02-07 18:44:27 +00:00
|
|
|
|
|
|
|
|
|
|
|
val _ =
|
|
|
|
Outer_Syntax.command @{command_keyword doc_class} "define document class"
|
|
|
|
(Parse_Spec.overloaded
|
|
|
|
-- (Parse.type_args_constrained -- Parse.binding)
|
|
|
|
-- (@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"})
|
2018-02-08 15:25:15 +00:00
|
|
|
-- Scan.repeat1 (Parse.const_binding -- Scan.option (@{keyword "<="} |-- Parse.term)))
|
|
|
|
-- Scan.repeat (@{keyword "where"} |-- Parse.term)
|
|
|
|
>> (fn (((overloaded, x), (y, z)),rex) =>
|
|
|
|
Toplevel.theory (add_record_cmd {overloaded = overloaded} x y z rex)));
|
|
|
|
|
|
|
|
*}
|
2018-02-28 13:06:52 +00:00
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
section{* Testing and Validation *}
|
|
|
|
|
2018-02-08 15:25:15 +00:00
|
|
|
ML{*
|
|
|
|
Binding.print;
|
|
|
|
Syntax.read_term;
|
2018-02-28 10:31:42 +00:00
|
|
|
Syntax.pretty_typ;
|
2018-02-08 15:25:15 +00:00
|
|
|
try;
|
|
|
|
|
2018-02-07 18:44:27 +00:00
|
|
|
*}
|
|
|
|
|
|
|
|
|
|
|
|
(* Look at this thingi ... *)
|
|
|
|
ML \<open>
|
|
|
|
fun document_command markdown (loc, txt) =
|
|
|
|
Toplevel.keep
|
|
|
|
(fn state => (case loc of
|
|
|
|
NONE => ignore (Thy_Output.output_text state markdown txt)
|
|
|
|
| SOME (_, pos) => error ("Illegal target specification -- not a theory context"
|
|
|
|
^ Position.here pos)))
|
|
|
|
o Toplevel.present_local_theory loc
|
|
|
|
(fn state => ignore (Thy_Output.output_text state markdown txt));
|
|
|
|
|
|
|
|
\<close>
|
2018-02-27 11:02:19 +00:00
|
|
|
|
|
|
|
text{* @{theory "Nat"}*}
|
|
|
|
ML\<open>
|
|
|
|
open Markup;
|
|
|
|
Markup.binding;
|
2018-02-28 10:31:42 +00:00
|
|
|
TFree;
|
|
|
|
open Position;
|
|
|
|
Position.line;
|
2018-02-28 13:06:52 +00:00
|
|
|
Context.Theory;
|
|
|
|
Context_Position.report_generic;
|
|
|
|
Context_Position.report;
|
2018-02-27 11:02:19 +00:00
|
|
|
\<close>
|
2018-02-07 18:44:27 +00:00
|
|
|
|
|
|
|
end
|