# HG changeset patch
# User wenzelm
# Date 1365187423 -7200
# Node ID e09446d3cacaca7ed22b966a1bd2a3976d7efdef
# Parent  bd3358aac5d20ad22cfae3cb4d9686e6e0816951
unified terminology with Markup.DOCUMENT_SOURCE in Scala, which is unused but displayed as "document source" entity in Isabelle/jEdit;

diff -r bd3358aac5d2 -r e09446d3caca src/Pure/PIDE/markup.ML
--- 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";
diff -r bd3358aac5d2 -r e09446d3caca src/Pure/Thy/thy_output.ML
--- 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)));