author | wenzelm |
Sun, 21 Aug 2022 11:48:14 +0200 | |
changeset 75939 | 87f0adcb7e10 |
parent 74567 | 40910c47d7a1 |
permissions | -rw-r--r-- |
69887 | 1 |
(* Title: Pure/Thy/document_marker.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Document markers: declarations on the presentation context. |
|
5 |
*) |
|
6 |
||
7 |
signature DOCUMENT_MARKER = |
|
8 |
sig |
|
9 |
type marker = Proof.context -> Proof.context |
|
69962
82e945d472d5
documentation of document markers and re-interpreted command tags;
wenzelm
parents:
69916
diff
changeset
|
10 |
val check: Proof.context -> string * Position.T -> string * (Token.src -> marker) |
69887 | 11 |
val setup: binding -> 'a context_parser -> ('a -> marker) -> theory -> theory |
69889
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69887
diff
changeset
|
12 |
val setup0: binding -> 'a parser -> ('a -> marker) -> theory -> theory |
70134 | 13 |
val evaluate: string -> Input.source -> marker |
14 |
val command_name: Proof.context -> string |
|
69891
def3ec9cdb7e
document markers are formal comments, and may thus occur anywhere in the command-span;
wenzelm
parents:
69890
diff
changeset
|
15 |
val legacy_tag: string -> Input.source |
69887 | 16 |
end; |
17 |
||
18 |
structure Document_Marker: DOCUMENT_MARKER = |
|
19 |
struct |
|
20 |
||
21 |
(* theory data *) |
|
22 |
||
23 |
type marker = Proof.context -> Proof.context; |
|
24 |
||
25 |
structure Markers = Theory_Data |
|
26 |
( |
|
27 |
type T = (Token.src -> Proof.context -> Proof.context) Name_Space.table; |
|
28 |
val empty : T = Name_Space.empty_table "document_marker"; |
|
29 |
val merge = Name_Space.merge_tables; |
|
30 |
); |
|
31 |
||
32 |
val get_markers = Markers.get o Proof_Context.theory_of; |
|
33 |
||
34 |
fun check ctxt = Name_Space.check (Context.Proof ctxt) (get_markers ctxt); |
|
35 |
||
36 |
fun setup name scan body thy = |
|
37 |
let |
|
38 |
fun marker src ctxt = |
|
39 |
let val (x, ctxt') = Token.syntax scan src ctxt |
|
40 |
in body x ctxt' end; |
|
41 |
in thy |> Markers.map (Name_Space.define (Context.Theory thy) true (name, marker) #> #2) end; |
|
42 |
||
69889
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69887
diff
changeset
|
43 |
fun setup0 name scan = setup name (Scan.lift scan); |
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69887
diff
changeset
|
44 |
|
69887 | 45 |
|
46 |
(* evaluate inner syntax *) |
|
47 |
||
70134 | 48 |
val config_command_name = Config.declare_string ("command_name", \<^here>) (K ""); |
49 |
val command_name = Config.apply config_command_name; |
|
50 |
||
69887 | 51 |
val parse_marker = Parse.token Parse.liberal_name ::: Parse.!!! Parse.args; |
52 |
||
70134 | 53 |
fun evaluate cmd_name input ctxt = |
69887 | 54 |
let |
69967 | 55 |
val syms = Input.source_explode input |
56 |
|> drop_prefix (fn (s, _) => s = Symbol.marker); |
|
57 |
val pos = #1 (Symbol_Pos.range syms); |
|
58 |
||
59 |
val _ = Context_Position.reports ctxt (map (pair pos) (Comment.kind_markups Comment.Marker)); |
|
60 |
||
74567 | 61 |
val keywords = Keyword.no_major_keywords (Thy_Header.get_keywords' ctxt); |
69967 | 62 |
val body = Symbol_Pos.cartouche_content syms; |
69887 | 63 |
val markers = |
74558 | 64 |
Input.source true (Symbol_Pos.implode body) (Symbol_Pos.range body) |
74564 | 65 |
|> Parse.read_embedded ctxt keywords (Parse.list parse_marker); |
70134 | 66 |
in |
67 |
ctxt |
|
68 |
|> Config.put config_command_name cmd_name |
|
69 |
|> fold (fn src => #2 (check ctxt (Token.name_of_src src)) src) markers |
|
70 |
|> Config.put config_command_name (command_name ctxt) |
|
71 |
end; |
|
72 |
||
73 |
||
74 |
(* tag with scope *) |
|
75 |
||
76 |
val parse_tag = |
|
77 |
Scan.state :|-- (fn context => |
|
78 |
let |
|
79 |
val ctxt = Context.proof_of context; |
|
80 |
val scope0 = |
|
81 |
if Keyword.is_theory_goal (Thy_Header.get_keywords' ctxt) (command_name ctxt) |
|
82 |
then Document_Source.Command |
|
83 |
else Document_Source.Proof; |
|
84 |
val tag = Scan.optional Document_Source.tag_scope scope0 -- Document_Source.tag_name >> swap; |
|
70135
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
70134
diff
changeset
|
85 |
in Scan.lift (Parse.position tag) end); |
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
70134
diff
changeset
|
86 |
|
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
70134
diff
changeset
|
87 |
fun update_tags (tag as (name, _), pos) ctxt = |
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
70134
diff
changeset
|
88 |
(Context_Position.report ctxt pos (Markup.document_tag name); |
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
70134
diff
changeset
|
89 |
Document_Source.update_tags tag ctxt); |
69887 | 90 |
|
91 |
||
92 |
(* concrete markers *) |
|
93 |
||
69889
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69887
diff
changeset
|
94 |
fun meta_data markup arg ctxt = |
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69887
diff
changeset
|
95 |
(Context_Position.report_text ctxt (Position.thread_data ()) markup arg; ctxt); |
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69887
diff
changeset
|
96 |
|
69887 | 97 |
val _ = |
98 |
Theory.setup |
|
70135
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
70134
diff
changeset
|
99 |
(setup (Binding.make ("tag", \<^here>)) parse_tag update_tags #> |
69889
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69887
diff
changeset
|
100 |
setup0 (Binding.make ("title", \<^here>)) Parse.embedded (meta_data Markup.meta_title) #> |
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69887
diff
changeset
|
101 |
setup0 (Binding.make ("creator", \<^here>)) Parse.embedded (meta_data Markup.meta_creator) #> |
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69887
diff
changeset
|
102 |
setup0 (Binding.make ("contributor", \<^here>)) Parse.embedded (meta_data Markup.meta_contributor) #> |
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69887
diff
changeset
|
103 |
setup0 (Binding.make ("date", \<^here>)) Parse.embedded (meta_data Markup.meta_date) #> |
69962
82e945d472d5
documentation of document markers and re-interpreted command tags;
wenzelm
parents:
69916
diff
changeset
|
104 |
setup0 (Binding.make ("license", \<^here>)) Parse.embedded (meta_data Markup.meta_license) #> |
70205 | 105 |
setup0 (Binding.make ("description", \<^here>)) Parse.embedded_input |
69890 | 106 |
(fn source => fn ctxt => |
107 |
let |
|
108 |
val (arg, pos) = Input.source_content source; |
|
109 |
val _ = Context_Position.report ctxt pos Markup.words; |
|
69962
82e945d472d5
documentation of document markers and re-interpreted command tags;
wenzelm
parents:
69916
diff
changeset
|
110 |
in meta_data Markup.meta_description arg ctxt end)); |
69887 | 111 |
|
69891
def3ec9cdb7e
document markers are formal comments, and may thus occur anywhere in the command-span;
wenzelm
parents:
69890
diff
changeset
|
112 |
fun legacy_tag name = |
70134 | 113 |
Input.string (cartouche ("tag (proof) " ^ Symbol_Pos.quote_string_qq name)); |
69891
def3ec9cdb7e
document markers are formal comments, and may thus occur anywhere in the command-span;
wenzelm
parents:
69890
diff
changeset
|
114 |
|
69887 | 115 |
end; |