author | wenzelm |
Fri, 26 Apr 2024 13:25:44 +0200 | |
changeset 80150 | 96f60533ec1d |
parent 73761 | ef1a18e20ace |
permissions | -rw-r--r-- |
72760
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Tools/doc.ML |
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
3 |
|
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
4 |
Access to Isabelle documentation. |
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
5 |
*) |
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
6 |
|
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
7 |
signature DOC = |
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
8 |
sig |
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
9 |
val check: Proof.context -> string * Position.T -> string |
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
10 |
end; |
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
11 |
|
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
12 |
structure Doc: DOC = |
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
13 |
struct |
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
14 |
|
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
15 |
fun check ctxt arg = |
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
16 |
Completion.check_item "documentation" (Markup.doc o #1) |
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
17 |
(\<^scala>\<open>doc_names\<close> "" |> split_lines |> map (rpair ())) ctxt arg; |
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
18 |
|
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
19 |
val _ = |
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
20 |
Theory.setup |
73761 | 21 |
(Document_Output.antiquotation_verbatim_embedded \<^binding>\<open>doc\<close> |
72760
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
22 |
(Scan.lift Parse.embedded_position) check); |
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
23 |
|
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
24 |
end; |