# HG changeset patch
# User wenzelm
# Date 1284737480 -7200
# Node ID cf61ec140c4dc51dab228fb63b937b52c22dad7d
# Parent  4301d70795d517d125c630112db6bd1165b4a9f3# Parent  73bcb12fdc69643b035539abd6257246b3f16e5e
merged

diff -r 4301d70795d5 -r cf61ec140c4d doc-src/IsarRef/Thy/document/Document_Preparation.tex
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Fri Sep 17 16:38:11 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Fri Sep 17 17:31:20 2010 +0200
@@ -164,6 +164,8 @@
     \indexdef{}{antiquotation}{const}\hypertarget{antiquotation.const}{\hyperlink{antiquotation.const}{\mbox{\isa{const}}}} & : & \isa{antiquotation} \\
     \indexdef{}{antiquotation}{abbrev}\hypertarget{antiquotation.abbrev}{\hyperlink{antiquotation.abbrev}{\mbox{\isa{abbrev}}}} & : & \isa{antiquotation} \\
     \indexdef{}{antiquotation}{typ}\hypertarget{antiquotation.typ}{\hyperlink{antiquotation.typ}{\mbox{\isa{typ}}}} & : & \isa{antiquotation} \\
+    \indexdef{}{antiquotation}{type}\hypertarget{antiquotation.type}{\hyperlink{antiquotation.type}{\mbox{\isa{type}}}} & : & \isa{antiquotation} \\
+    \indexdef{}{antiquotation}{class}\hypertarget{antiquotation.class}{\hyperlink{antiquotation.class}{\mbox{\isa{class}}}} & : & \isa{antiquotation} \\
     \indexdef{}{antiquotation}{text}\hypertarget{antiquotation.text}{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}} & : & \isa{antiquotation} \\
     \indexdef{}{antiquotation}{goals}\hypertarget{antiquotation.goals}{\hyperlink{antiquotation.goals}{\mbox{\isa{goals}}}} & : & \isa{antiquotation} \\
     \indexdef{}{antiquotation}{subgoals}\hypertarget{antiquotation.subgoals}{\hyperlink{antiquotation.subgoals}{\mbox{\isa{subgoals}}}} & : & \isa{antiquotation} \\
@@ -208,6 +210,8 @@
       'const' options term |
       'abbrev' options term |
       'typ' options type |
+      'type' options name |
+      'class' options name |
       'text' options name |
       'goals' options |
       'subgoals' options |
@@ -259,8 +263,14 @@
   
   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}abbrev\ c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isacharbraceright}{\isachardoublequote}} prints a constant abbreviation
   \isa{{\isachardoublequote}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ rhs{\isachardoublequote}} as defined in the current context.
+
   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typ\ {\isasymtau}{\isacharbraceright}{\isachardoublequote}} prints a well-formed type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}.
-  
+
+  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}type\ {\isasymkappa}{\isacharbraceright}{\isachardoublequote}} prints a type constructor
+    (logical or abbreviation) \isa{{\isachardoublequote}{\isasymkappa}{\isachardoublequote}}.
+
+  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}class\ c{\isacharbraceright}{\isachardoublequote}} prints a class \isa{c}.
+
   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}text\ s{\isacharbraceright}{\isachardoublequote}} prints uninterpreted source text \isa{s}.  This is particularly useful to print portions of text according
   to the Isabelle document style, without demanding well-formedness,
   e.g.\ small pieces of terms that should not be parsed or
diff -r 4301d70795d5 -r cf61ec140c4d src/HOL/Power.thy
--- a/src/HOL/Power.thy	Fri Sep 17 16:38:11 2010 +0200
+++ b/src/HOL/Power.thy	Fri Sep 17 17:31:20 2010 +0200
@@ -29,7 +29,7 @@
 context monoid_mult
 begin
 
-subclass power ..
+subclass power .
 
 lemma power_one [simp]:
   "1 ^ n = 1"
diff -r 4301d70795d5 -r cf61ec140c4d src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Fri Sep 17 16:38:11 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Fri Sep 17 17:31:20 2010 +0200
@@ -791,7 +791,7 @@
     "k < l \<Longrightarrow> divmod_rel k l 0 k"
   | "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"
 
-code_pred divmod_rel ..
+code_pred divmod_rel .
 thm divmod_rel.equation
 value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
 
diff -r 4301d70795d5 -r cf61ec140c4d src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Fri Sep 17 16:38:11 2010 +0200
+++ b/src/Pure/General/binding.ML	Fri Sep 17 17:31:20 2010 +0200
@@ -124,10 +124,8 @@
 (* str_of *)
 
 fun str_of binding =
-  let
-    val text = qualified_name_of binding;
-    val props = Position.properties_of (pos_of binding);
-  in Markup.markup (Markup.properties props (Markup.binding (name_of binding))) text end;
+  qualified_name_of binding
+  |> Markup.markup (Position.markup (pos_of binding) (Markup.binding (name_of binding)));
 
 end;
 end;
diff -r 4301d70795d5 -r cf61ec140c4d src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Fri Sep 17 16:38:11 2010 +0200
+++ b/src/Pure/General/markup.ML	Fri Sep 17 17:31:20 2010 +0200
@@ -30,7 +30,6 @@
   val position_properties': string list
   val position_properties: string list
   val positionN: string val position: T
-  val locationN: string val location: T
   val indentN: string
   val blockN: string val block: int -> T
   val widthN: string
@@ -120,6 +119,7 @@
   val promptN: string val prompt: T
   val readyN: string val ready: T
   val reportN: string val report: T
+  val no_reportN: string val no_report: T
   val badN: string val bad: T
   val no_output: output * output
   val default_output: T -> output * output
@@ -194,7 +194,6 @@
 val position_properties = [lineN, columnN, offsetN] @ position_properties';
 
 val (positionN, position) = markup_elem "position";
-val (locationN, location) = markup_elem "location";
 
 
 (* pretty printing *)
@@ -348,6 +347,7 @@
 val (readyN, ready) = markup_elem "ready";
 
 val (reportN, report) = markup_elem "report";
+val (no_reportN, no_report) = markup_elem "no_report";
 
 val (badN, bad) = markup_elem "bad";
 
diff -r 4301d70795d5 -r cf61ec140c4d src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Fri Sep 17 16:38:11 2010 +0200
+++ b/src/Pure/General/markup.scala	Fri Sep 17 17:31:20 2010 +0200
@@ -90,7 +90,6 @@
     Set(LINE, COLUMN, OFFSET, END_LINE, END_COLUMN, END_OFFSET, FILE, ID)
 
   val POSITION = "position"
-  val LOCATION = "location"
 
 
   /* pretty printing */
@@ -236,7 +235,6 @@
 
   val INIT = "init"
   val STATUS = "status"
-  val REPORT = "report"
   val WRITELN = "writeln"
   val TRACING = "tracing"
   val WARNING = "warning"
@@ -249,6 +247,9 @@
   val SIGNAL = "signal"
   val EXIT = "exit"
 
+  val REPORT = "report"
+  val NO_REPORT = "no_report"
+
   val BAD = "bad"
 
   val Ready = Markup("ready", Nil)
diff -r 4301d70795d5 -r cf61ec140c4d src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Fri Sep 17 16:38:11 2010 +0200
+++ b/src/Pure/General/position.ML	Fri Sep 17 17:31:20 2010 +0200
@@ -27,7 +27,8 @@
   val of_properties: Properties.T -> T
   val properties_of: T -> Properties.T
   val default_properties: T -> Properties.T -> Properties.T
-  val report_markup: T -> Markup.T
+  val markup: T -> Markup.T -> Markup.T
+  val reported_text: Markup.T -> T -> string -> string
   val report_text: Markup.T -> T -> string -> unit
   val report: Markup.T -> T -> unit
   val str_of: T -> string
@@ -126,12 +127,16 @@
   if exists (member (op =) Markup.position_properties o #1) props then props
   else properties_of default @ props;
 
-fun report_markup pos = Markup.properties (properties_of pos) Markup.report;
+val markup = Markup.properties o properties_of;
+
+
+(* reports *)
 
-fun report_text markup (pos as Pos (count, _)) txt =
-  if invalid_count count then ()
-  else Output.report (Markup.markup (Markup.properties (properties_of pos) markup) txt);
+fun reported_text m (pos as Pos (count, _)) txt =
+  if invalid_count count then ""
+  else Markup.markup (markup pos m) txt;
 
+fun report_text markup pos txt = Output.report (reported_text markup pos txt);
 fun report markup pos = report_text markup pos "";
 
 
diff -r 4301d70795d5 -r cf61ec140c4d src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri Sep 17 16:38:11 2010 +0200
+++ b/src/Pure/Isar/class.ML	Fri Sep 17 17:31:20 2010 +0200
@@ -630,7 +630,8 @@
   end;
 
 fun default_intro_tac ctxt [] =
-      intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt []
+      COND Thm.no_prems no_tac
+        (intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt [])
   | default_intro_tac _ _ = no_tac;
 
 fun default_tac rules ctxt facts =
diff -r 4301d70795d5 -r cf61ec140c4d src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Sep 17 16:38:11 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Sep 17 17:31:20 2010 +0200
@@ -734,8 +734,8 @@
 local
 
 fun parse_failed ctxt pos msg kind =
- (Context_Position.report ctxt Markup.bad pos;
-  cat_error msg ("Failed to parse " ^ kind));
+  cat_error msg ("Failed to parse " ^ kind ^
+    Markup.markup Markup.report (Context_Position.reported_text ctxt Markup.bad pos ""));
 
 fun parse_sort ctxt text =
   let
diff -r 4301d70795d5 -r cf61ec140c4d src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Fri Sep 17 16:38:11 2010 +0200
+++ b/src/Pure/Isar/runtime.ML	Fri Sep 17 17:31:20 2010 +0200
@@ -61,7 +61,7 @@
           Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
         | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn
         | EXCURSION_FAIL (exn, loc) =>
-            map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs context exn)
+            map (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)) (exn_msgs context exn)
         | TERMINATE => ["Exit"]
         | TimeLimit.TimeOut => ["Timeout"]
         | TOPLEVEL_ERROR => ["Error"]
diff -r 4301d70795d5 -r cf61ec140c4d src/Pure/ML/ml_compiler_polyml-5.3.ML
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Fri Sep 17 16:38:11 2010 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Fri Sep 17 17:31:20 2010 +0200
@@ -49,7 +49,7 @@
 
     fun report_decl markup loc decl =
       report_text Markup.ML_ref (offset_position_of loc)
-        (Markup.markup (Markup.properties (Position.properties_of (position_of decl)) markup) "");
+        (Markup.markup (Position.markup (position_of decl) markup) "");
     fun report loc (PolyML.PTtype types) =
           PolyML.NameSpace.displayTypeExpression (types, depth, space)
           |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
@@ -121,10 +121,10 @@
     fun message {message = msg, hard, location = loc, context = _} =
       let
         val txt =
-          Markup.markup Markup.location
+          Markup.markup Markup.no_report
             ((if hard then "Error" else "Warning") ^ Position.str_of (position_of loc) ^ ":\n") ^
           Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
-          Markup.markup (Position.report_markup (offset_position_of loc)) "";
+          Position.reported_text Markup.report (offset_position_of loc) "";
       in if hard then err txt else warn txt end;
 
 
diff -r 4301d70795d5 -r cf61ec140c4d src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Fri Sep 17 16:38:11 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Fri Sep 17 17:31:20 2010 +0200
@@ -60,8 +60,10 @@
           atts match {
             case Markup.Serial(i) =>
               val result = XML.Elem(Markup(name, Position.purge(atts)), body)
-              (add_result(i, result) /: Isar_Document.reported_positions(command, message))(
-                (st, range) => st.add_markup(Text.Info(range, result)))
+              val st1 =
+                (add_result(i, result) /: Isar_Document.message_positions(command, message))(
+                  (st, range) => st.add_markup(Text.Info(range, result)))
+              (st1 /: Isar_Document.message_reports(message))(_ accumulate _)
             case _ => System.err.println("Ignored message without serial number: " + message); this
           }
       }
diff -r 4301d70795d5 -r cf61ec140c4d src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Fri Sep 17 16:38:11 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Fri Sep 17 17:31:20 2010 +0200
@@ -56,30 +56,42 @@
   }
 
 
+  /* result messages */
+
+  def clean_message(body: XML.Body): XML.Body =
+    body filter { case XML.Elem(Markup(Markup.NO_REPORT, _), _) => false case _ => true } map
+      { case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts)) case t => t }
+
+  def message_reports(msg: XML.Tree): List[XML.Elem] =
+    msg match {
+      case elem @ XML.Elem(Markup(Markup.REPORT, _), _) => List(elem)
+      case XML.Elem(_, body) => body.flatMap(message_reports)
+      case XML.Text(_) => Nil
+    }
+
+
   /* reported positions */
 
-  private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
-  private val exclude_pos = Set(Markup.LOCATION)
-
-  private def is_state(msg: XML.Tree): Boolean =
+  def is_state(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.WRITELN, _), List(XML.Elem(Markup(Markup.STATE, _), _))) => true
       case _ => false
     }
 
-  def reported_positions(command: Command, message: XML.Elem): Set[Text.Range] =
+  private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
+
+  def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =
   {
-    def reported(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
+    def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
       tree match {
         case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
         if include_pos(name) && id == command.id =>
           val range = command.decode(raw_range).restrict(command.range)
-          body.foldLeft(if (range.is_singularity) set else set + range)(reported)
-        case XML.Elem(Markup(name, _), body) if !exclude_pos(name) =>
-          body.foldLeft(set)(reported)
+          body.foldLeft(if (range.is_singularity) set else set + range)(positions)
+        case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(positions)
         case _ => set
       }
-    val set = reported(Set.empty, message)
+    val set = positions(Set.empty, message)
     if (set.isEmpty && !is_state(message))
       set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))
     else set
diff -r 4301d70795d5 -r cf61ec140c4d src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Fri Sep 17 16:38:11 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Fri Sep 17 17:31:20 2010 +0200
@@ -100,7 +100,8 @@
     if (pid.isEmpty && kind == Markup.INIT)
       pid = props.find(_._1 == Markup.PID).map(_._1)
 
-    xml_cache.cache_tree(XML.Elem(Markup(kind, props), body))((message: XML.Tree) =>
+    val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
+    xml_cache.cache_tree(msg)((message: XML.Tree) =>
       receiver ! new Result(message.asInstanceOf[XML.Elem]))
   }
 
diff -r 4301d70795d5 -r cf61ec140c4d src/Pure/context_position.ML
--- a/src/Pure/context_position.ML	Fri Sep 17 16:38:11 2010 +0200
+++ b/src/Pure/context_position.ML	Fri Sep 17 17:31:20 2010 +0200
@@ -10,6 +10,7 @@
   val set_visible: bool -> Proof.context -> Proof.context
   val restore_visible: Proof.context -> Proof.context -> Proof.context
   val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit
+  val reported_text: Proof.context -> Markup.T -> Position.T -> string -> string
   val report_text: Proof.context -> Markup.T -> Position.T -> string -> unit
   val report: Proof.context -> Markup.T -> Position.T -> unit
 end;
@@ -29,9 +30,10 @@
 
 fun if_visible ctxt f x = if is_visible ctxt then f x else ();
 
-fun report_text ctxt markup pos txt =
-  if is_visible ctxt then Position.report_text markup pos txt else ();
+fun reported_text ctxt markup pos txt =
+  if is_visible ctxt then Position.reported_text markup pos txt else "";
 
+fun report_text ctxt markup pos txt = Output.report (reported_text ctxt markup pos txt);
 fun report ctxt markup pos = report_text ctxt markup pos "";
 
 end;
diff -r 4301d70795d5 -r cf61ec140c4d src/Tools/jEdit/dist-template/etc/isabelle-jedit.css
--- a/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Fri Sep 17 16:38:11 2010 +0200
+++ b/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Fri Sep 17 17:31:20 2010 +0200
@@ -8,7 +8,7 @@
 .error { background-color: #FFC1C1; }
 .debug { background-color: #FFE4E1; }
 
-.location { display: none; }
+.report { display: none; }
 
 .hilite { background-color: #FFFACD; }