# HG changeset patch
# User wenzelm
# Date 1355570917 -3600
# Node ID 42bbe637be546420f38d19d8b90f1abf193deddc
# Parent  58bd88159f8f2ac9d15b29302de3642efb9876be
fold main goal;

diff -r 58bd88159f8f -r 42bbe637be54 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sat Dec 15 12:16:16 2012 +0100
+++ b/src/Pure/PIDE/markup.ML	Sat Dec 15 12:28:37 2012 +0100
@@ -95,6 +95,7 @@
   val subgoalsN: string
   val proof_stateN: string val proof_state: int -> T
   val stateN: string val state: T
+  val goalN: string val goal: T
   val subgoalN: string val subgoal: string -> T
   val taskN: string
   val acceptedN: string val accepted: T
@@ -337,6 +338,7 @@
 val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
 
 val (stateN, state) = markup_elem "state";
+val (goalN, goal) = markup_elem "goal";
 val (subgoalN, subgoal) = markup_string "subgoal" nameN;
 
 
diff -r 58bd88159f8f -r 42bbe637be54 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sat Dec 15 12:16:16 2012 +0100
+++ b/src/Pure/PIDE/markup.scala	Sat Dec 15 12:28:37 2012 +0100
@@ -210,6 +210,7 @@
   val PROOF_STATE = "proof_state"
 
   val STATE = "state"
+  val GOAL = "goal"
   val SUBGOAL = "subgoal"
 
 
diff -r 58bd88159f8f -r 42bbe637be54 src/Pure/goal_display.ML
--- a/src/Pure/goal_display.ML	Sat Dec 15 12:16:16 2012 +0100
+++ b/src/Pure/goal_display.ML	Sat Dec 15 12:28:37 2012 +0100
@@ -130,7 +130,7 @@
     val (As, B) = Logic.strip_horn prop;
     val ngoals = length As;
   in
-    (if show_main_goal then [prt_term B] else []) @
+    (if show_main_goal then [Pretty.mark Markup.goal (prt_term B)] else []) @
      (if ngoals = 0 then [Pretty.str "No subgoals!"]
       else if ngoals > goals_limit then
         pretty_subgoals (take goals_limit As) @
diff -r 58bd88159f8f -r 42bbe637be54 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Sat Dec 15 12:16:16 2012 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Sat Dec 15 12:28:37 2012 +0100
@@ -531,7 +531,7 @@
 
   /* nested text structure -- folds */
 
-  private val fold_depth_include = Set(Markup.SUBGOAL)
+  private val fold_depth_include = Set(Markup.GOAL, Markup.SUBGOAL)
 
   def fold_depth(range: Text.Range): Stream[Text.Info[Int]] =
     snapshot.cumulate_markup[Int](range, 0, Some(fold_depth_include), _ =>