1.1 --- a/src/Pure/General/markup.ML Thu Aug 26 10:42:22 2010 +0200
1.2 +++ b/src/Pure/General/markup.ML Thu Aug 26 11:33:36 2010 +0200
1.3 @@ -99,6 +99,8 @@
1.4 val command_spanN: string val command_span: string -> T
1.5 val ignored_spanN: string val ignored_span: T
1.6 val malformed_spanN: string val malformed_span: T
1.7 + val subgoalsN: string
1.8 + val proof_stateN: string val proof_state: int -> T
1.9 val stateN: string val state: T
1.10 val subgoalN: string val subgoal: T
1.11 val sendbackN: string val sendback: T
1.12 @@ -156,16 +158,13 @@
1.13 fun markup_int elem prop = (elem, fn i => (elem, [(prop, print_int i)]): T);
1.14
1.15
1.16 -(* name *)
1.17 +(* misc properties *)
1.18
1.19 val nameN = "name";
1.20 fun name a = properties [(nameN, a)];
1.21
1.22 val (bindingN, binding) = markup_string "binding" nameN;
1.23
1.24 -
1.25 -(* kind *)
1.26 -
1.27 val kindN = "kind";
1.28
1.29
1.30 @@ -305,6 +304,9 @@
1.31
1.32 (* toplevel *)
1.33
1.34 +val subgoalsN = "subgoals";
1.35 +val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
1.36 +
1.37 val (stateN, state) = markup_elem "state";
1.38 val (subgoalN, subgoal) = markup_elem "subgoal";
1.39 val (sendbackN, sendback) = markup_elem "sendback";
2.1 --- a/src/Pure/General/markup.scala Thu Aug 26 10:42:22 2010 +0200
2.2 +++ b/src/Pure/General/markup.scala Thu Aug 26 11:33:36 2010 +0200
2.3 @@ -9,7 +9,7 @@
2.4
2.5 object Markup
2.6 {
2.7 - /* integers */
2.8 + /* plain values */
2.9
2.10 object Int {
2.11 def apply(i: scala.Int): String = i.toString
2.12 @@ -26,25 +26,33 @@
2.13 }
2.14
2.15
2.16 - /* property values */
2.17 + /* named properties */
2.18
2.19 - def get_string(name: String, props: List[(String, String)]): Option[String] =
2.20 - props.find(p => p._1 == name).map(_._2)
2.21 -
2.22 - def get_long(name: String, props: List[(String, String)]): Option[scala.Long] =
2.23 + class Property(val name: String)
2.24 {
2.25 - get_string(name, props) match {
2.26 - case None => None
2.27 - case Some(Long(i)) => Some(i)
2.28 - }
2.29 + def apply(value: String): List[(String, String)] = List((name, value))
2.30 + def unapply(props: List[(String, String)]): Option[String] =
2.31 + props.find(_._1 == name).map(_._2)
2.32 }
2.33
2.34 - def get_int(name: String, props: List[(String, String)]): Option[scala.Int] =
2.35 + class Int_Property(name: String)
2.36 {
2.37 - get_string(name, props) match {
2.38 - case None => None
2.39 - case Some(Int(i)) => Some(i)
2.40 - }
2.41 + def apply(value: scala.Int): List[(String, String)] = List((name, Int(value)))
2.42 + def unapply(props: List[(String, String)]): Option[Int] =
2.43 + props.find(_._1 == name) match {
2.44 + case None => None
2.45 + case Some((_, value)) => Int.unapply(value)
2.46 + }
2.47 + }
2.48 +
2.49 + class Long_Property(name: String)
2.50 + {
2.51 + def apply(value: scala.Long): List[(String, String)] = List((name, Long(value)))
2.52 + def unapply(props: List[(String, String)]): Option[Long] =
2.53 + props.find(_._1 == name) match {
2.54 + case None => None
2.55 + case Some((_, value)) => Long.unapply(value)
2.56 + }
2.57 }
2.58
2.59
2.60 @@ -53,7 +61,7 @@
2.61 val Empty = Markup("", Nil)
2.62
2.63
2.64 - /* name */
2.65 + /* misc properties */
2.66
2.67 val NAME = "name"
2.68 val KIND = "kind"
2.69 @@ -86,9 +94,9 @@
2.70
2.71 /* pretty printing */
2.72
2.73 - val INDENT = "indent"
2.74 + val Indent = new Int_Property("indent")
2.75 val BLOCK = "block"
2.76 - val WIDTH = "width"
2.77 + val Width = new Int_Property("width")
2.78 val BREAK = "break"
2.79
2.80
2.81 @@ -188,6 +196,9 @@
2.82
2.83 /* toplevel */
2.84
2.85 + val SUBGOALS = "subgoals"
2.86 + val PROOF_STATE = "proof_state"
2.87 +
2.88 val STATE = "state"
2.89 val SUBGOAL = "subgoal"
2.90 val SENDBACK = "sendback"
3.1 --- a/src/Pure/General/position.scala Thu Aug 26 10:42:22 2010 +0200
3.2 +++ b/src/Pure/General/position.scala Thu Aug 26 11:33:36 2010 +0200
3.3 @@ -11,22 +11,21 @@
3.4 {
3.5 type T = List[(String, String)]
3.6
3.7 - def get_line(pos: T): Option[Int] = Markup.get_int(Markup.LINE, pos)
3.8 - def get_column(pos: T): Option[Int] = Markup.get_int(Markup.COLUMN, pos)
3.9 - def get_offset(pos: T): Option[Int] = Markup.get_int(Markup.OFFSET, pos)
3.10 - def get_end_line(pos: T): Option[Int] = Markup.get_int(Markup.END_LINE, pos)
3.11 - def get_end_column(pos: T): Option[Int] = Markup.get_int(Markup.END_COLUMN, pos)
3.12 - def get_end_offset(pos: T): Option[Int] = Markup.get_int(Markup.END_OFFSET, pos)
3.13 - def get_file(pos: T): Option[String] = Markup.get_string(Markup.FILE, pos)
3.14 - def get_id(pos: T): Option[Long] = Markup.get_long(Markup.ID, pos)
3.15 + val Line = new Markup.Int_Property(Markup.LINE)
3.16 + val End_Line = new Markup.Int_Property(Markup.END_LINE)
3.17 + val Offset = new Markup.Int_Property(Markup.OFFSET)
3.18 + val End_Offset = new Markup.Int_Property(Markup.END_OFFSET)
3.19 + val File = new Markup.Property(Markup.FILE)
3.20 + val Id = new Markup.Long_Property(Markup.ID)
3.21
3.22 - def get_range(pos: T): Option[Text.Range] =
3.23 - (get_offset(pos), get_end_offset(pos)) match {
3.24 - case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
3.25 - case (Some(start), None) => Some(Text.Range(start))
3.26 - case (_, _) => None
3.27 - }
3.28 -
3.29 - object Id { def unapply(pos: T): Option[Long] = get_id(pos) }
3.30 - object Range { def unapply(pos: T): Option[Text.Range] = get_range(pos) }
3.31 + object Range
3.32 + {
3.33 + def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop)
3.34 + def unapply(pos: T): Option[Text.Range] =
3.35 + (Offset.unapply(pos), End_Offset.unapply(pos)) match {
3.36 + case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
3.37 + case (Some(start), None) => Some(Text.Range(start))
3.38 + case _ => None
3.39 + }
3.40 + }
3.41 }
4.1 --- a/src/Pure/General/pretty.scala Thu Aug 26 10:42:22 2010 +0200
4.2 +++ b/src/Pure/General/pretty.scala Thu Aug 26 11:33:36 2010 +0200
4.3 @@ -19,12 +19,11 @@
4.4 object Block
4.5 {
4.6 def apply(i: Int, body: XML.Body): XML.Tree =
4.7 - XML.Elem(Markup(Markup.BLOCK, List((Markup.INDENT, Markup.Int(i)))), body)
4.8 + XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body)
4.9
4.10 def unapply(tree: XML.Tree): Option[(Int, XML.Body)] =
4.11 tree match {
4.12 - case XML.Elem(
4.13 - Markup(Markup.BLOCK, List((Markup.INDENT, Markup.Int(i)))), body) => Some((i, body))
4.14 + case XML.Elem(Markup(Markup.BLOCK, Markup.Indent(i)), body) => Some((i, body))
4.15 case _ => None
4.16 }
4.17 }
4.18 @@ -32,12 +31,11 @@
4.19 object Break
4.20 {
4.21 def apply(w: Int): XML.Tree =
4.22 - XML.Elem(
4.23 - Markup(Markup.BREAK, List((Markup.WIDTH, Markup.Int(w)))), List(XML.Text(Symbol.spaces(w))))
4.24 + XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), List(XML.Text(Symbol.spaces(w))))
4.25
4.26 def unapply(tree: XML.Tree): Option[Int] =
4.27 tree match {
4.28 - case XML.Elem(Markup(Markup.BREAK, List((Markup.WIDTH, Markup.Int(w)))), _) => Some(w)
4.29 + case XML.Elem(Markup(Markup.BREAK, Markup.Width(w)), _) => Some(w)
4.30 case _ => None
4.31 }
4.32 }
5.1 --- a/src/Pure/Isar/proof.ML Thu Aug 26 10:42:22 2010 +0200
5.2 +++ b/src/Pure/Isar/proof.ML Thu Aug 26 11:33:36 2010 +0200
5.3 @@ -42,6 +42,7 @@
5.4 val raw_goal: state -> {context: context, facts: thm list, goal: thm}
5.5 val goal: state -> {context: context, facts: thm list, goal: thm}
5.6 val simple_goal: state -> {context: context, goal: thm}
5.7 + val status_markup: state -> Markup.T
5.8 val let_bind: (term list * term) list -> state -> state
5.9 val let_bind_cmd: (string list * string) list -> state -> state
5.10 val write: Syntax.mode -> (term * mixfix) list -> state -> state
5.11 @@ -520,6 +521,11 @@
5.12 val (ctxt, (_, goal)) = get_goal (refine_insert facts state);
5.13 in {context = ctxt, goal = goal} end;
5.14
5.15 +fun status_markup state =
5.16 + (case try goal state of
5.17 + SOME {goal, ...} => Markup.proof_state (Thm.nprems_of goal)
5.18 + | NONE => Markup.empty);
5.19 +
5.20
5.21
5.22 (*** structured proof commands ***)
6.1 --- a/src/Pure/Isar/toplevel.ML Thu Aug 26 10:42:22 2010 +0200
6.2 +++ b/src/Pure/Isar/toplevel.ML Thu Aug 26 11:33:36 2010 +0200
6.3 @@ -563,13 +563,6 @@
6.4 fun status tr m =
6.5 setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) ();
6.6
6.7 -fun async_state (tr as Transition {print, ...}) st =
6.8 - if print then
6.9 - ignore
6.10 - (Future.fork (fn () =>
6.11 - setmp_thread_position tr (fn () => Future.status (fn () => print_state false st)) ()))
6.12 - else ();
6.13 -
6.14 fun error_msg tr exn_info =
6.15 setmp_thread_position tr (fn () =>
6.16 Output.error_msg (ML_Compiler.exn_message (EXCURSION_FAIL exn_info))) ();
6.17 @@ -628,6 +621,22 @@
6.18
6.19 (* managed execution *)
6.20
6.21 +local
6.22 +
6.23 +fun async_state (tr as Transition {print, ...}) st =
6.24 + if print then
6.25 + ignore
6.26 + (Future.fork (fn () =>
6.27 + setmp_thread_position tr (fn () => Future.status (fn () => print_state false st)) ()))
6.28 + else ();
6.29 +
6.30 +fun proof_status tr st =
6.31 + (case try proof_of st of
6.32 + SOME prf => status tr (Proof.status_markup prf)
6.33 + | NONE => ());
6.34 +
6.35 +in
6.36 +
6.37 fun run_command thy_name tr st =
6.38 (case
6.39 (case init_of tr of
6.40 @@ -637,13 +646,18 @@
6.41 let val int = is_some (init_of tr) in
6.42 (case transition int tr st of
6.43 SOME (st', NONE) =>
6.44 - (status tr Markup.finished; if int then () else async_state tr st'; SOME st')
6.45 + (status tr Markup.finished;
6.46 + proof_status tr st';
6.47 + if int then () else async_state tr st';
6.48 + SOME st')
6.49 | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn
6.50 | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
6.51 | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE))
6.52 end
6.53 | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));
6.54
6.55 +end;
6.56 +
6.57
6.58 (* nested commands *)
6.59
7.1 --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Thu Aug 26 10:42:22 2010 +0200
7.2 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Thu Aug 26 11:33:36 2010 +0200
7.3 @@ -44,13 +44,18 @@
7.4
7.5 fun report_parse_tree depth space =
7.6 let
7.7 + val report_text =
7.8 + (case Context.thread_data () of
7.9 + SOME (Context.Proof ctxt) => Context_Position.report_text ctxt
7.10 + | _ => Position.report_text);
7.11 +
7.12 fun report_decl markup loc decl =
7.13 - Position.report_text Markup.ML_ref (position_of loc)
7.14 + report_text Markup.ML_ref (position_of loc)
7.15 (Markup.markup (Markup.properties (Position.properties_of (position_of decl)) markup) "");
7.16 fun report loc (PolyML.PTtype types) =
7.17 PolyML.NameSpace.displayTypeExpression (types, depth, space)
7.18 |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
7.19 - |> Position.report_text Markup.ML_typing (position_of loc)
7.20 + |> report_text Markup.ML_typing (position_of loc)
7.21 | report loc (PolyML.PTdeclaredAt decl) = report_decl Markup.ML_def loc decl
7.22 | report loc (PolyML.PTopenedAt decl) = report_decl Markup.ML_open loc decl
7.23 | report loc (PolyML.PTstructureAt decl) = report_decl Markup.ML_struct loc decl
8.1 --- a/src/Pure/ML/ml_context.ML Thu Aug 26 10:42:22 2010 +0200
8.2 +++ b/src/Pure/ML/ml_context.ML Thu Aug 26 11:33:36 2010 +0200
8.3 @@ -166,7 +166,9 @@
8.4 fun eval verbose pos ants =
8.5 let
8.6 (*prepare source text*)
8.7 - val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ());
8.8 + val ((env, body), env_ctxt) =
8.9 + eval_antiquotes (ants, pos) (Context.thread_data ())
8.10 + ||> Option.map (Context.mapping I (Context_Position.set_visible false));
8.11 val _ =
8.12 if ! trace then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
8.13 else ();
9.1 --- a/src/Pure/PIDE/command.scala Thu Aug 26 10:42:22 2010 +0200
9.2 +++ b/src/Pure/PIDE/command.scala Thu Aug 26 11:33:36 2010 +0200
9.3 @@ -46,11 +46,11 @@
9.4 case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
9.5 (this /: msgs)((state, msg) =>
9.6 msg match {
9.7 - case XML.Elem(Markup(name, atts), args)
9.8 - if Position.get_id(atts) == Some(command.id) && Position.get_range(atts).isDefined =>
9.9 - val range = command.decode(Position.get_range(atts).get)
9.10 + case XML.Elem(Markup(name, atts @ Position.Range(range)), args)
9.11 + if Position.Id.unapply(atts) == Some(command.id) =>
9.12 val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
9.13 - val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
9.14 + val info =
9.15 + Text.Info[Any](command.decode(range), XML.Elem(Markup(name, props), args))
9.16 state.add_markup(info)
9.17 case _ => System.err.println("Ignored report message: " + msg); state
9.18 })
10.1 --- a/src/Pure/PIDE/markup_tree.scala Thu Aug 26 10:42:22 2010 +0200
10.2 +++ b/src/Pure/PIDE/markup_tree.scala Thu Aug 26 11:33:36 2010 +0200
10.3 @@ -115,7 +115,10 @@
10.4 if (last < stop) parent.restrict(Text.Range(last, stop)) #:: nexts
10.5 else nexts
10.6
10.7 - case Nil => Stream(Text.Info(Text.Range(last, root_range.stop), default))
10.8 + case Nil =>
10.9 + val stop = root_range.stop
10.10 + if (last < stop) Stream(Text.Info(Text.Range(last, stop), default))
10.11 + else Stream.empty
10.12 }
10.13 }
10.14 stream(root_range.start, List((Text.Info(root_range, default), overlapping(root_range))))
11.1 --- a/src/Pure/PIDE/text.scala Thu Aug 26 10:42:22 2010 +0200
11.2 +++ b/src/Pure/PIDE/text.scala Thu Aug 26 11:33:36 2010 +0200
11.3 @@ -33,7 +33,7 @@
11.4 def +(i: Offset): Range = map(_ + i)
11.5 def -(i: Offset): Range = map(_ - i)
11.6
11.7 - def is_singleton: Boolean = start == stop
11.8 + def is_singularity: Boolean = start == stop
11.9
11.10 def contains(i: Offset): Boolean = start == i || start < i && i < stop
11.11 def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop
12.1 --- a/src/Pure/System/session.scala Thu Aug 26 10:42:22 2010 +0200
12.2 +++ b/src/Pure/System/session.scala Thu Aug 26 11:33:36 2010 +0200
12.3 @@ -131,15 +131,15 @@
12.4 {
12.5 raw_protocol.event(result)
12.6
12.7 - Position.get_id(result.properties) match {
12.8 - case Some(state_id) =>
12.9 + result.properties match {
12.10 + case Position.Id(state_id) =>
12.11 try {
12.12 val (st, state) = global_state.accumulate(state_id, result.message)
12.13 global_state = state
12.14 indicate_command_change(st.command)
12.15 }
12.16 catch { case _: Document.State.Fail => bad_result(result) }
12.17 - case None =>
12.18 + case _ =>
12.19 if (result.is_status) {
12.20 result.body match {
12.21 case List(Isar_Document.Assign(id, edits)) =>
13.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Thu Aug 26 10:42:22 2010 +0200
13.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Thu Aug 26 11:33:36 2010 +0200
13.3 @@ -55,11 +55,11 @@
13.4 val Text.Range(begin, end) = snapshot.convert(info_range + command_start)
13.5 val line = buffer.getLineOfOffset(begin)
13.6
13.7 - (Position.get_file(props), Position.get_line(props)) match {
13.8 + (Position.File.unapply(props), Position.Line.unapply(props)) match {
13.9 case (Some(ref_file), Some(ref_line)) =>
13.10 new External_Hyperlink(begin, end, line, ref_file, ref_line)
13.11 case _ =>
13.12 - (Position.get_id(props), Position.get_offset(props)) match {
13.13 + (Position.Id.unapply(props), Position.Offset.unapply(props)) match {
13.14 case (Some(ref_id), Some(ref_offset)) =>
13.15 snapshot.lookup_command(ref_id) match {
13.16 case Some(ref_cmd) =>