tuned markup, e.g. relevant for Rendering.tooltip;
--- 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.
--- 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 =
--- 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 =