# 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 \ divmod_rel k l 0 k" | "k \ l \ divmod_rel (k - l) l q r \ 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; }