--- 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";
--- 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"
--- 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
+ }
+ }
}
--- 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
}
}
--- 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 ***)
--- 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 *)
--- 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
--- 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 ();
--- 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
})
--- 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))))
--- 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
--- 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)) =>
--- 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) =>