obsolete;

--- a/src/Pure/Isar/proof.ML	Wed Jul 13 15:19:16 2016 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Jul 13 15:23:33 2016 +0200
@@ -42,7 +42,6 @@
   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
@@ -561,11 +560,6 @@
     val (ctxt, (_, goal)) = get_goal (refine_insert using 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);
-
 fun method_error kind pos state =
   Seq.single (Proof_Display.method_error kind pos (raw_goal state));
 

--- a/src/Pure/PIDE/command.ML	Wed Jul 13 15:19:16 2016 +0200
+++ b/src/Pure/PIDE/command.ML	Wed Jul 13 15:23:33 2016 +0200
@@ -209,11 +209,6 @@
 fun status tr m =
   Toplevel.setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
 
-fun proof_status tr st =
-  (case try Toplevel.proof_of st of
-    SOME prf => status tr (Proof.status_markup prf)
-  | NONE => ());
-
 fun command_indent tr st =
   (case try Toplevel.proof_of st of
     SOME prf =>
@@ -251,7 +246,6 @@
         in {failed = true, command = tr, state = st} end
     | SOME st' =>
         let
-          val _ = proof_status tr st';
           val _ = status tr Markup.finished;
         in {failed = false, command = tr, state = st'} end)
   end;

--- a/src/Pure/PIDE/markup.ML	Wed Jul 13 15:19:16 2016 +0200
+++ b/src/Pure/PIDE/markup.ML	Wed Jul 13 15:23:33 2016 +0200
@@ -156,8 +156,6 @@
     Properties.T -> ({file: string, offset: int, name: string} * Time.time) option
   val timingN: string val timing: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> T
   val command_indentN: string val command_indent: int -> T
-  val subgoalsN: string
-  val proof_stateN: string val proof_state: int -> T
   val goalN: string val goal: T
   val subgoalN: string val subgoal: string -> T
   val taskN: string
@@ -584,9 +582,6 @@
 
 (* goals *)
 
-val subgoalsN = "subgoals";
-val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
-
 val (goalN, goal) = markup_elem "goal";
 val (subgoalN, subgoal) = markup_string "subgoal" nameN;
 

--- a/src/Pure/PIDE/markup.scala	Wed Jul 13 15:19:16 2016 +0200
+++ b/src/Pure/PIDE/markup.scala	Wed Jul 13 15:23:33 2016 +0200
@@ -384,9 +384,6 @@
 
   /* goals */
 
-  val SUBGOALS = "subgoals"
-  val PROOF_STATE = "proof_state"
-
   val GOAL = "goal"
   val SUBGOAL = "subgoal"