unified terminology with Markup.DOCUMENT_SOURCE in Scala, which is unused but displayed as "document source" entity in Isabelle/jEdit;
--- a/src/Pure/PIDE/markup.ML Fri Apr 05 18:31:35 2013 +0200
+++ b/src/Pure/PIDE/markup.ML Fri Apr 05 20:43:43 2013 +0200
@@ -72,7 +72,7 @@
val ML_structN: string
val ML_typingN: string val ML_typing: T
val ML_sourceN: string val ML_source: T
- val doc_sourceN: string val doc_source: T
+ val document_sourceN: string val document_source: T
val antiqN: string val antiq: T
val ML_antiquotationN: string
val document_antiquotationN: string
@@ -305,7 +305,7 @@
(* embedded source text *)
val (ML_sourceN, ML_source) = markup_elem "ML_source";
-val (doc_sourceN, doc_source) = markup_elem "doc_source";
+val (document_sourceN, document_source) = markup_elem "document_source";
val (antiqN, antiq) = markup_elem "antiq";
val ML_antiquotationN = "ML_antiquotation";
--- a/src/Pure/Thy/thy_output.ML Fri Apr 05 18:31:35 2013 +0200
+++ b/src/Pure/Thy/thy_output.ML Fri Apr 05 20:43:43 2013 +0200
@@ -205,7 +205,7 @@
fun check_text (txt, pos) state =
- (Position.report pos Markup.doc_source;
+ (Position.report pos Markup.document_source;
if Toplevel.is_skipped_proof state then ()
else ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));