obsolete;
authorwenzelm
Wed Jul 13 15:23:33 2016 +0200 (2016-07-13)
changeset 6347531016a88197b
parent 63474 f66e3c3b0fb1
child 63476 ff1d86b07751
obsolete;
src/Pure/Isar/proof.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Jul 13 15:19:16 2016 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Jul 13 15:23:33 2016 +0200
     1.3 @@ -42,7 +42,6 @@
     1.4    val raw_goal: state -> {context: context, facts: thm list, goal: thm}
     1.5    val goal: state -> {context: context, facts: thm list, goal: thm}
     1.6    val simple_goal: state -> {context: context, goal: thm}
     1.7 -  val status_markup: state -> Markup.T
     1.8    val let_bind: (term list * term) list -> state -> state
     1.9    val let_bind_cmd: (string list * string) list -> state -> state
    1.10    val write: Syntax.mode -> (term * mixfix) list -> state -> state
    1.11 @@ -561,11 +560,6 @@
    1.12      val (ctxt, (_, goal)) = get_goal (refine_insert using state);
    1.13    in {context = ctxt, goal = goal} end;
    1.14  
    1.15 -fun status_markup state =
    1.16 -  (case try goal state of
    1.17 -    SOME {goal, ...} => Markup.proof_state (Thm.nprems_of goal)
    1.18 -  | NONE => Markup.empty);
    1.19 -
    1.20  fun method_error kind pos state =
    1.21    Seq.single (Proof_Display.method_error kind pos (raw_goal state));
    1.22  
     2.1 --- a/src/Pure/PIDE/command.ML	Wed Jul 13 15:19:16 2016 +0200
     2.2 +++ b/src/Pure/PIDE/command.ML	Wed Jul 13 15:23:33 2016 +0200
     2.3 @@ -209,11 +209,6 @@
     2.4  fun status tr m =
     2.5    Toplevel.setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
     2.6  
     2.7 -fun proof_status tr st =
     2.8 -  (case try Toplevel.proof_of st of
     2.9 -    SOME prf => status tr (Proof.status_markup prf)
    2.10 -  | NONE => ());
    2.11 -
    2.12  fun command_indent tr st =
    2.13    (case try Toplevel.proof_of st of
    2.14      SOME prf =>
    2.15 @@ -251,7 +246,6 @@
    2.16          in {failed = true, command = tr, state = st} end
    2.17      | SOME st' =>
    2.18          let
    2.19 -          val _ = proof_status tr st';
    2.20            val _ = status tr Markup.finished;
    2.21          in {failed = false, command = tr, state = st'} end)
    2.22    end;
     3.1 --- a/src/Pure/PIDE/markup.ML	Wed Jul 13 15:19:16 2016 +0200
     3.2 +++ b/src/Pure/PIDE/markup.ML	Wed Jul 13 15:23:33 2016 +0200
     3.3 @@ -156,8 +156,6 @@
     3.4      Properties.T -> ({file: string, offset: int, name: string} * Time.time) option
     3.5    val timingN: string val timing: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> T
     3.6    val command_indentN: string val command_indent: int -> T
     3.7 -  val subgoalsN: string
     3.8 -  val proof_stateN: string val proof_state: int -> T
     3.9    val goalN: string val goal: T
    3.10    val subgoalN: string val subgoal: string -> T
    3.11    val taskN: string
    3.12 @@ -584,9 +582,6 @@
    3.13  
    3.14  (* goals *)
    3.15  
    3.16 -val subgoalsN = "subgoals";
    3.17 -val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
    3.18 -
    3.19  val (goalN, goal) = markup_elem "goal";
    3.20  val (subgoalN, subgoal) = markup_string "subgoal" nameN;
    3.21  
     4.1 --- a/src/Pure/PIDE/markup.scala	Wed Jul 13 15:19:16 2016 +0200
     4.2 +++ b/src/Pure/PIDE/markup.scala	Wed Jul 13 15:23:33 2016 +0200
     4.3 @@ -384,9 +384,6 @@
     4.4  
     4.5    /* goals */
     4.6  
     4.7 -  val SUBGOALS = "subgoals"
     4.8 -  val PROOF_STATE = "proof_state"
     4.9 -
    4.10    val GOAL = "goal"
    4.11    val SUBGOAL = "subgoal"
    4.12