# HG changeset patch
# User wenzelm
# Date 1453470362 -3600
# Node ID 25f4a9cd8b682f6fa1b46a26ffbae38a26a2a69b
# Parent  949d2c9f6ff786256f09c712e58a04baa14fbc42
tuned markup, e.g. relevant for Rendering.tooltip;

diff -r 949d2c9f6ff7 -r 25f4a9cd8b68 NEWS
--- a/NEWS	Thu Jan 21 22:16:48 2016 +0100
+++ b/NEWS	Fri Jan 22 14:46:02 2016 +0100
@@ -178,8 +178,8 @@
 * Antiquotation @{verbatim [display]} supports option "indent".
 
 * Antiquotation @{theory_text} prints uninterpreted theory source text
-(outer syntax with command keywords etc.). This may be used in the short
-form \<^theory_text>\<open>...\<close>. @{theory_text [display]} supports option "indent".
+(Isar outer syntax with command keywords etc.). This may be used in the
+short form \<^theory_text>\<open>...\<close>. @{theory_text [display]} supports option "indent".
 
 * Antiquotation @{doc ENTRY} provides a reference to the given
 documentation, with a hyperlink in the Prover IDE.
diff -r 949d2c9f6ff7 -r 25f4a9cd8b68 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Thu Jan 21 22:16:48 2016 +0100
+++ b/src/Pure/PIDE/markup.ML	Fri Jan 22 14:46:02 2016 +0100
@@ -28,7 +28,7 @@
   val is_delimited: Properties.T -> bool
   val language: {name: string, symbols: bool, antiquotes: bool, delimited: bool} -> T
   val language': {name: string, symbols: bool, antiquotes: bool} -> bool -> T
-  val language_outer: bool -> T
+  val language_Isar: bool -> T
   val language_method: T
   val language_attribute: T
   val language_sort: bool -> T
@@ -301,7 +301,7 @@
 fun language' {name, symbols, antiquotes} delimited =
   language {name = name, symbols = symbols, antiquotes = antiquotes, delimited = delimited};
 
-val language_outer = language' {name = "", symbols = true, antiquotes = false};
+val language_Isar = language' {name = "Isar", symbols = true, antiquotes = false};
 val language_method =
   language {name = "method", symbols = true, antiquotes = false, delimited = false};
 val language_attribute =
diff -r 949d2c9f6ff7 -r 25f4a9cd8b68 src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Thu Jan 21 22:16:48 2016 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML	Fri Jan 22 14:46:02 2016 +0100
@@ -87,7 +87,7 @@
         let
           val _ =
             Context_Position.report ctxt (Input.pos_of source)
-              (Markup.language_outer (Input.is_delimited source));
+              (Markup.language_Isar (Input.is_delimited source));
 
           val keywords = Thy_Header.get_keywords' ctxt;
           val toks =