--- a/src/Pure/PIDE/markup.ML Tue Feb 18 20:37:45 2014 +0100
+++ b/src/Pure/PIDE/markup.ML Tue Feb 18 20:50:07 2014 +0100
@@ -27,6 +27,7 @@
val language_prop: T
val language_ML: T
val language_document: T
+ val language_text: T
val bindingN: string val binding: T
val entityN: string val entity: string -> string -> T
val get_entity_kind: T -> string option
@@ -253,6 +254,7 @@
val language_ML = language "ML";
val language_document = language "document";
+val language_text = language "text";
(* formal entities *)
--- a/src/Pure/Thy/thy_output.ML Tue Feb 18 20:37:45 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Tue Feb 18 20:50:07 2014 +0100
@@ -470,6 +470,9 @@
fun pretty_text ctxt =
Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o split_lines;
+fun pretty_text_report ctxt (s, pos) =
+ (Context_Position.report ctxt pos Markup.language_text; pretty_text ctxt s);
+
fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
@@ -574,7 +577,7 @@
basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
basic_entity (Binding.name "class") (Scan.lift Args.name_inner_syntax) pretty_class #>
basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
- basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
+ basic_entity (Binding.name "text") (Scan.lift (Parse.position Args.name)) pretty_text_report #>
basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #>
basic_entity (Binding.name "theory") (Scan.lift (Parse.position Args.name)) pretty_theory);