| author | wenzelm |
| Wed, 25 Jun 2025 13:32:28 +0200 | |
| changeset 82767 | 3b045cc57f0c |
| parent 82759 | c7d2ae25d008 |
| 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 |
| 82767 | 9 |
val names: unit -> string list |
|
72760
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
10 |
val check: Proof.context -> string * Position.T -> string |
|
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
11 |
end; |
|
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
12 |
|
|
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
13 |
structure Doc: DOC = |
|
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
14 |
struct |
|
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
15 |
|
| 82767 | 16 |
fun names () = split_lines (\<^scala>\<open>doc_names\<close> ML_System.platform); |
17 |
||
|
72760
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
18 |
fun check ctxt arg = |
|
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
19 |
Completion.check_item "documentation" (Markup.doc o #1) |
| 82767 | 20 |
(map (rpair ()) (names ())) ctxt arg; |
|
72760
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
21 |
|
|
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
22 |
val _ = |
|
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
23 |
Theory.setup |
| 73761 | 24 |
(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
|
25 |
(Scan.lift Parse.embedded_position) check); |
|
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
26 |
|
|
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
diff
changeset
|
27 |
end; |