| author | wenzelm |
| Fri, 25 Aug 2023 15:31:14 +0200 | |
| changeset 78577 | a945b541efff |
| parent 73761 | ef1a18e20ace |
| child 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 |
|
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; |