# HG changeset patch
# User wenzelm
# Date 1355511908 -3600
# Node ID 08ce81aeeacc834f75815827a35c7d96b85f1818
# Parent  6bb47864ae4589db3daba74b3ff424dc4299fe9e
more subgoal markup information, which is potentially useful to manage proof state output;

diff -r 6bb47864ae45 -r 08ce81aeeacc src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Dec 14 18:41:56 2012 +0100
+++ b/src/Pure/PIDE/markup.ML	Fri Dec 14 20:05:08 2012 +0100
@@ -95,7 +95,7 @@
   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 subgoalN: string val subgoal: string -> T
   val taskN: string
   val acceptedN: string val accepted: T
   val forkedN: string val forked: T
@@ -337,7 +337,7 @@
 val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
 
 val (stateN, state) = markup_elem "state";
-val (subgoalN, subgoal) = markup_elem "subgoal";
+val (subgoalN, subgoal) = markup_string "subgoal" nameN;
 
 
 (* command status *)
diff -r 6bb47864ae45 -r 08ce81aeeacc src/Pure/goal_display.ML
--- a/src/Pure/goal_display.ML	Fri Dec 14 18:41:56 2012 +0100
+++ b/src/Pure/goal_display.ML	Fri Dec 14 20:05:08 2012 +0100
@@ -115,9 +115,9 @@
     fun pretty_list _ _ [] = []
       | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
 
-    fun pretty_subgoal (n, A) =
-      Pretty.markup Markup.subgoal [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A];
-    fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
+    fun pretty_subgoal s A =
+      Pretty.markup (Markup.subgoal s) [Pretty.str (" " ^ s ^ ". "), prt_term A];
+    val pretty_subgoals = map_index (fn (i, A) => pretty_subgoal (string_of_int (i + 1)) A);
 
     val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt);