# HG changeset patch # User wenzelm # Date 1282815216 -7200 # Node ID 0ab848f84accc02e553f074e2714c19b489c0755 # Parent 3913f58d0fcc39c84694162b071c44e660ef4470# Parent 6d5f9af42eca42d3e5f594e03ad3e74f15415e2e merged diff -r 3913f58d0fcc -r 0ab848f84acc src/Pure/General/markup.ML --- a/src/Pure/General/markup.ML Thu Aug 26 10:42:22 2010 +0200 +++ b/src/Pure/General/markup.ML Thu Aug 26 11:33:36 2010 +0200 @@ -99,6 +99,8 @@ val command_spanN: string val command_span: string -> T val ignored_spanN: string val ignored_span: T val malformed_spanN: string val malformed_span: T + val subgoalsN: string + val proof_stateN: string val proof_state: int -> T val stateN: string val state: T val subgoalN: string val subgoal: T val sendbackN: string val sendback: T @@ -156,16 +158,13 @@ fun markup_int elem prop = (elem, fn i => (elem, [(prop, print_int i)]): T); -(* name *) +(* misc properties *) val nameN = "name"; fun name a = properties [(nameN, a)]; val (bindingN, binding) = markup_string "binding" nameN; - -(* kind *) - val kindN = "kind"; @@ -305,6 +304,9 @@ (* toplevel *) +val subgoalsN = "subgoals"; +val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN; + val (stateN, state) = markup_elem "state"; val (subgoalN, subgoal) = markup_elem "subgoal"; val (sendbackN, sendback) = markup_elem "sendback"; diff -r 3913f58d0fcc -r 0ab848f84acc src/Pure/General/markup.scala --- a/src/Pure/General/markup.scala Thu Aug 26 10:42:22 2010 +0200 +++ b/src/Pure/General/markup.scala Thu Aug 26 11:33:36 2010 +0200 @@ -9,7 +9,7 @@ object Markup { - /* integers */ + /* plain values */ object Int { def apply(i: scala.Int): String = i.toString @@ -26,25 +26,33 @@ } - /* property values */ - - def get_string(name: String, props: List[(String, String)]): Option[String] = - props.find(p => p._1 == name).map(_._2) + /* named properties */ - def get_long(name: String, props: List[(String, String)]): Option[scala.Long] = + class Property(val name: String) { - get_string(name, props) match { - case None => None - case Some(Long(i)) => Some(i) - } + def apply(value: String): List[(String, String)] = List((name, value)) + def unapply(props: List[(String, String)]): Option[String] = + props.find(_._1 == name).map(_._2) } - def get_int(name: String, props: List[(String, String)]): Option[scala.Int] = + class Int_Property(name: String) { - get_string(name, props) match { - case None => None - case Some(Int(i)) => Some(i) - } + def apply(value: scala.Int): List[(String, String)] = List((name, Int(value))) + def unapply(props: List[(String, String)]): Option[Int] = + props.find(_._1 == name) match { + case None => None + case Some((_, value)) => Int.unapply(value) + } + } + + class Long_Property(name: String) + { + def apply(value: scala.Long): List[(String, String)] = List((name, Long(value))) + def unapply(props: List[(String, String)]): Option[Long] = + props.find(_._1 == name) match { + case None => None + case Some((_, value)) => Long.unapply(value) + } } @@ -53,7 +61,7 @@ val Empty = Markup("", Nil) - /* name */ + /* misc properties */ val NAME = "name" val KIND = "kind" @@ -86,9 +94,9 @@ /* pretty printing */ - val INDENT = "indent" + val Indent = new Int_Property("indent") val BLOCK = "block" - val WIDTH = "width" + val Width = new Int_Property("width") val BREAK = "break" @@ -188,6 +196,9 @@ /* toplevel */ + val SUBGOALS = "subgoals" + val PROOF_STATE = "proof_state" + val STATE = "state" val SUBGOAL = "subgoal" val SENDBACK = "sendback" diff -r 3913f58d0fcc -r 0ab848f84acc src/Pure/General/position.scala --- a/src/Pure/General/position.scala Thu Aug 26 10:42:22 2010 +0200 +++ b/src/Pure/General/position.scala Thu Aug 26 11:33:36 2010 +0200 @@ -11,22 +11,21 @@ { type T = List[(String, String)] - def get_line(pos: T): Option[Int] = Markup.get_int(Markup.LINE, pos) - def get_column(pos: T): Option[Int] = Markup.get_int(Markup.COLUMN, pos) - def get_offset(pos: T): Option[Int] = Markup.get_int(Markup.OFFSET, pos) - def get_end_line(pos: T): Option[Int] = Markup.get_int(Markup.END_LINE, pos) - def get_end_column(pos: T): Option[Int] = Markup.get_int(Markup.END_COLUMN, pos) - def get_end_offset(pos: T): Option[Int] = Markup.get_int(Markup.END_OFFSET, pos) - def get_file(pos: T): Option[String] = Markup.get_string(Markup.FILE, pos) - def get_id(pos: T): Option[Long] = Markup.get_long(Markup.ID, pos) + val Line = new Markup.Int_Property(Markup.LINE) + val End_Line = new Markup.Int_Property(Markup.END_LINE) + val Offset = new Markup.Int_Property(Markup.OFFSET) + val End_Offset = new Markup.Int_Property(Markup.END_OFFSET) + val File = new Markup.Property(Markup.FILE) + val Id = new Markup.Long_Property(Markup.ID) - def get_range(pos: T): Option[Text.Range] = - (get_offset(pos), get_end_offset(pos)) match { - case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop)) - case (Some(start), None) => Some(Text.Range(start)) - case (_, _) => None - } - - object Id { def unapply(pos: T): Option[Long] = get_id(pos) } - object Range { def unapply(pos: T): Option[Text.Range] = get_range(pos) } + object Range + { + def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop) + def unapply(pos: T): Option[Text.Range] = + (Offset.unapply(pos), End_Offset.unapply(pos)) match { + case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop)) + case (Some(start), None) => Some(Text.Range(start)) + case _ => None + } + } } diff -r 3913f58d0fcc -r 0ab848f84acc src/Pure/General/pretty.scala --- a/src/Pure/General/pretty.scala Thu Aug 26 10:42:22 2010 +0200 +++ b/src/Pure/General/pretty.scala Thu Aug 26 11:33:36 2010 +0200 @@ -19,12 +19,11 @@ object Block { def apply(i: Int, body: XML.Body): XML.Tree = - XML.Elem(Markup(Markup.BLOCK, List((Markup.INDENT, Markup.Int(i)))), body) + XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body) def unapply(tree: XML.Tree): Option[(Int, XML.Body)] = tree match { - case XML.Elem( - Markup(Markup.BLOCK, List((Markup.INDENT, Markup.Int(i)))), body) => Some((i, body)) + case XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body) => Some((i, body)) case _ => None } } @@ -32,12 +31,11 @@ object Break { def apply(w: Int): XML.Tree = - XML.Elem( - Markup(Markup.BREAK, List((Markup.WIDTH, Markup.Int(w)))), List(XML.Text(Symbol.spaces(w)))) + XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), List(XML.Text(Symbol.spaces(w)))) def unapply(tree: XML.Tree): Option[Int] = tree match { - case XML.Elem(Markup(Markup.BREAK, List((Markup.WIDTH, Markup.Int(w)))), _) => Some(w) + case XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), _) => Some(w) case _ => None } } diff -r 3913f58d0fcc -r 0ab848f84acc src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Thu Aug 26 10:42:22 2010 +0200 +++ b/src/Pure/Isar/proof.ML Thu Aug 26 11:33:36 2010 +0200 @@ -42,6 +42,7 @@ val raw_goal: state -> {context: context, facts: thm list, goal: thm} val goal: state -> {context: context, facts: thm list, goal: thm} val simple_goal: state -> {context: context, goal: thm} + val status_markup: state -> Markup.T val let_bind: (term list * term) list -> state -> state val let_bind_cmd: (string list * string) list -> state -> state val write: Syntax.mode -> (term * mixfix) list -> state -> state @@ -520,6 +521,11 @@ val (ctxt, (_, goal)) = get_goal (refine_insert facts state); in {context = ctxt, goal = goal} end; +fun status_markup state = + (case try goal state of + SOME {goal, ...} => Markup.proof_state (Thm.nprems_of goal) + | NONE => Markup.empty); + (*** structured proof commands ***) diff -r 3913f58d0fcc -r 0ab848f84acc src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Thu Aug 26 10:42:22 2010 +0200 +++ b/src/Pure/Isar/toplevel.ML Thu Aug 26 11:33:36 2010 +0200 @@ -563,13 +563,6 @@ fun status tr m = setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) (); -fun async_state (tr as Transition {print, ...}) st = - if print then - ignore - (Future.fork (fn () => - setmp_thread_position tr (fn () => Future.status (fn () => print_state false st)) ())) - else (); - fun error_msg tr exn_info = setmp_thread_position tr (fn () => Output.error_msg (ML_Compiler.exn_message (EXCURSION_FAIL exn_info))) (); @@ -628,6 +621,22 @@ (* managed execution *) +local + +fun async_state (tr as Transition {print, ...}) st = + if print then + ignore + (Future.fork (fn () => + setmp_thread_position tr (fn () => Future.status (fn () => print_state false st)) ())) + else (); + +fun proof_status tr st = + (case try proof_of st of + SOME prf => status tr (Proof.status_markup prf) + | NONE => ()); + +in + fun run_command thy_name tr st = (case (case init_of tr of @@ -637,13 +646,18 @@ let val int = is_some (init_of tr) in (case transition int tr st of SOME (st', NONE) => - (status tr Markup.finished; if int then () else async_state tr st'; SOME st') + (status tr Markup.finished; + proof_status tr st'; + if int then () else async_state tr st'; + SOME st') | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE) | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE)) end | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE)); +end; + (* nested commands *) diff -r 3913f58d0fcc -r 0ab848f84acc src/Pure/ML/ml_compiler_polyml-5.3.ML --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Thu Aug 26 10:42:22 2010 +0200 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Thu Aug 26 11:33:36 2010 +0200 @@ -44,13 +44,18 @@ fun report_parse_tree depth space = let + val report_text = + (case Context.thread_data () of + SOME (Context.Proof ctxt) => Context_Position.report_text ctxt + | _ => Position.report_text); + fun report_decl markup loc decl = - Position.report_text Markup.ML_ref (position_of loc) + report_text Markup.ML_ref (position_of loc) (Markup.markup (Markup.properties (Position.properties_of (position_of decl)) markup) ""); fun report loc (PolyML.PTtype types) = PolyML.NameSpace.displayTypeExpression (types, depth, space) |> pretty_ml |> Pretty.from_ML |> Pretty.string_of - |> Position.report_text Markup.ML_typing (position_of loc) + |> report_text Markup.ML_typing (position_of loc) | report loc (PolyML.PTdeclaredAt decl) = report_decl Markup.ML_def loc decl | report loc (PolyML.PTopenedAt decl) = report_decl Markup.ML_open loc decl | report loc (PolyML.PTstructureAt decl) = report_decl Markup.ML_struct loc decl diff -r 3913f58d0fcc -r 0ab848f84acc src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Thu Aug 26 10:42:22 2010 +0200 +++ b/src/Pure/ML/ml_context.ML Thu Aug 26 11:33:36 2010 +0200 @@ -166,7 +166,9 @@ fun eval verbose pos ants = let (*prepare source text*) - val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ()); + val ((env, body), env_ctxt) = + eval_antiquotes (ants, pos) (Context.thread_data ()) + ||> Option.map (Context.mapping I (Context_Position.set_visible false)); val _ = if ! trace then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body]) else (); diff -r 3913f58d0fcc -r 0ab848f84acc src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Thu Aug 26 10:42:22 2010 +0200 +++ b/src/Pure/PIDE/command.scala Thu Aug 26 11:33:36 2010 +0200 @@ -46,11 +46,11 @@ case XML.Elem(Markup(Markup.REPORT, _), msgs) => (this /: msgs)((state, msg) => msg match { - case XML.Elem(Markup(name, atts), args) - if Position.get_id(atts) == Some(command.id) && Position.get_range(atts).isDefined => - val range = command.decode(Position.get_range(atts).get) + case XML.Elem(Markup(name, atts @ Position.Range(range)), args) + if Position.Id.unapply(atts) == Some(command.id) => val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1)) - val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args)) + val info = + Text.Info[Any](command.decode(range), XML.Elem(Markup(name, props), args)) state.add_markup(info) case _ => System.err.println("Ignored report message: " + msg); state }) diff -r 3913f58d0fcc -r 0ab848f84acc src/Pure/PIDE/markup_tree.scala --- a/src/Pure/PIDE/markup_tree.scala Thu Aug 26 10:42:22 2010 +0200 +++ b/src/Pure/PIDE/markup_tree.scala Thu Aug 26 11:33:36 2010 +0200 @@ -115,7 +115,10 @@ if (last < stop) parent.restrict(Text.Range(last, stop)) #:: nexts else nexts - case Nil => Stream(Text.Info(Text.Range(last, root_range.stop), default)) + case Nil => + val stop = root_range.stop + if (last < stop) Stream(Text.Info(Text.Range(last, stop), default)) + else Stream.empty } } stream(root_range.start, List((Text.Info(root_range, default), overlapping(root_range)))) diff -r 3913f58d0fcc -r 0ab848f84acc src/Pure/PIDE/text.scala --- a/src/Pure/PIDE/text.scala Thu Aug 26 10:42:22 2010 +0200 +++ b/src/Pure/PIDE/text.scala Thu Aug 26 11:33:36 2010 +0200 @@ -33,7 +33,7 @@ def +(i: Offset): Range = map(_ + i) def -(i: Offset): Range = map(_ - i) - def is_singleton: Boolean = start == stop + def is_singularity: Boolean = start == stop def contains(i: Offset): Boolean = start == i || start < i && i < stop def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop diff -r 3913f58d0fcc -r 0ab848f84acc src/Pure/System/session.scala --- a/src/Pure/System/session.scala Thu Aug 26 10:42:22 2010 +0200 +++ b/src/Pure/System/session.scala Thu Aug 26 11:33:36 2010 +0200 @@ -131,15 +131,15 @@ { raw_protocol.event(result) - Position.get_id(result.properties) match { - case Some(state_id) => + result.properties match { + case Position.Id(state_id) => try { val (st, state) = global_state.accumulate(state_id, result.message) global_state = state indicate_command_change(st.command) } catch { case _: Document.State.Fail => bad_result(result) } - case None => + case _ => if (result.is_status) { result.body match { case List(Isar_Document.Assign(id, edits)) => diff -r 3913f58d0fcc -r 0ab848f84acc src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Thu Aug 26 10:42:22 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Thu Aug 26 11:33:36 2010 +0200 @@ -55,11 +55,11 @@ val Text.Range(begin, end) = snapshot.convert(info_range + command_start) val line = buffer.getLineOfOffset(begin) - (Position.get_file(props), Position.get_line(props)) match { + (Position.File.unapply(props), Position.Line.unapply(props)) match { case (Some(ref_file), Some(ref_line)) => new External_Hyperlink(begin, end, line, ref_file, ref_line) case _ => - (Position.get_id(props), Position.get_offset(props)) match { + (Position.Id.unapply(props), Position.Offset.unapply(props)) match { case (Some(ref_id), Some(ref_offset)) => snapshot.lookup_command(ref_id) match { case Some(ref_cmd) =>