--- a/src/HOL/Tools/Nitpick/nitpick.ML Fri Sep 14 17:37:19 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Sep 14 18:12:41 2012 +0200
@@ -245,7 +245,7 @@
if mode = Auto_Try then
Unsynchronized.change state_ref o Proof.goal_message o K
o Pretty.chunks o cons (Pretty.str "") o single
- o Pretty.mark Isabelle_Markup.hilite
+ o Pretty.mark Isabelle_Markup.intensify
else
print o Pretty.string_of
val pprint_a = pprint Output.urgent_message
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Sep 14 17:37:19 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Sep 14 18:12:41 2012 +0200
@@ -137,7 +137,7 @@
|> outcome_code = someN
? Proof.goal_message (fn () =>
[Pretty.str "",
- Pretty.mark Isabelle_Markup.hilite (Pretty.str (message ()))]
+ Pretty.mark Isabelle_Markup.intensify (Pretty.str (message ()))]
|> Pretty.chunks))
end
else if blocking then
--- a/src/HOL/Tools/try0.ML Fri Sep 14 17:37:19 2012 +0200
+++ b/src/HOL/Tools/try0.ML Fri Sep 14 18:12:41 2012 +0200
@@ -146,7 +146,7 @@
(true, (s, st |> (if mode = Auto_Try then
Proof.goal_message
(fn () => Pretty.chunks [Pretty.str "",
- Pretty.markup Isabelle_Markup.hilite
+ Pretty.markup Isabelle_Markup.intensify
[Pretty.str message]])
else
tap (fn _ => Output.urgent_message message))))
--- a/src/Pure/General/name_space.ML Fri Sep 14 17:37:19 2012 +0200
+++ b/src/Pure/General/name_space.ML Fri Sep 14 18:12:41 2012 +0200
@@ -133,7 +133,7 @@
fun markup (Name_Space {kind, entries, ...}) name =
(case Symtab.lookup entries name of
- NONE => Isabelle_Markup.hilite
+ NONE => Isabelle_Markup.intensify
| SOME (_, entry) => entry_markup false kind (name, entry));
fun is_concealed space name = #concealed (the_entry space name);
--- a/src/Pure/PIDE/isabelle_markup.ML Fri Sep 14 17:37:19 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.ML Fri Sep 14 18:12:41 2012 +0200
@@ -84,7 +84,7 @@
val stateN: string val state: Markup.T
val subgoalN: string val subgoal: Markup.T
val sendbackN: string val sendback: Markup.T
- val hiliteN: string val hilite: Markup.T
+ val intensifyN: string val intensify: Markup.T
val taskN: string
val acceptedN: string val accepted: Markup.T
val forkedN: string val forked: Markup.T
@@ -264,7 +264,7 @@
val (stateN, state) = markup_elem "state";
val (subgoalN, subgoal) = markup_elem "subgoal";
val (sendbackN, sendback) = markup_elem "sendback";
-val (hiliteN, hilite) = markup_elem "hilite";
+val (intensifyN, intensify) = markup_elem "intensify";
(* command status *)
--- a/src/Pure/PIDE/isabelle_markup.scala Fri Sep 14 17:37:19 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala Fri Sep 14 18:12:41 2012 +0200
@@ -185,7 +185,7 @@
val STATE = "state"
val SUBGOAL = "subgoal"
val SENDBACK = "sendback"
- val HILITE = "hilite"
+ val INTENSIFY = "intensify"
/* command status */
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Fri Sep 14 17:37:19 2012 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Fri Sep 14 18:12:41 2012 +0200
@@ -41,7 +41,7 @@
if null ts then Markup.no_output
else if name = Isabelle_Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
else if name = Isabelle_Markup.sendbackN then (special "W", special "X")
- else if name = Isabelle_Markup.hiliteN then (special "0", special "1")
+ else if name = Isabelle_Markup.intensifyN then (special "0", special "1")
else if name = Isabelle_Markup.tfreeN then (special "C", special "A")
else if name = Isabelle_Markup.tvarN then (special "D", special "A")
else if name = Isabelle_Markup.freeN then (special "E", special "A")
--- a/src/Pure/Syntax/syntax_phases.ML Fri Sep 14 17:37:19 2012 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Fri Sep 14 18:12:41 2012 +0200
@@ -586,7 +586,7 @@
val m =
if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt
then Isabelle_Markup.fixed x
- else Isabelle_Markup.hilite;
+ else Isabelle_Markup.intensify;
in
if can Name.dest_skolem x
then ([m, Isabelle_Markup.skolem], Variable.revert_fixed ctxt x)
--- a/src/Tools/jEdit/etc/isabelle-jedit.css Fri Sep 14 17:37:19 2012 +0200
+++ b/src/Tools/jEdit/etc/isabelle-jedit.css Fri Sep 14 18:12:41 2012 +0200
@@ -9,7 +9,7 @@
.report { display: none; }
-.hilite { background-color: #FFCC66; }
+.intensify { background-color: #FFCC66; }
.keyword { font-weight: bold; color: #009966; }
.operator { font-weight: bold; }
--- a/src/Tools/jEdit/etc/options Fri Sep 14 17:37:19 2012 +0200
+++ b/src/Tools/jEdit/etc/options Fri Sep 14 18:12:41 2012 +0200
@@ -32,9 +32,9 @@
option error_color : string = "B22222FF"
option error1_color : string = "B2222232"
option bad_color : string = "FF6A6A64"
-option hilite_color : string = "FFCC6664"
+option intensify_color : string = "FFCC6664"
option quoted_color : string = "8B8B8B19"
-option subexp_color : string = "50505032"
+option highlight_color : string = "50505032"
option hyperlink_color : string = "000000FF"
option keyword1_color : string = "006699FF"
option keyword2_color : string = "009966FF"
--- a/src/Tools/jEdit/src/document_view.scala Fri Sep 14 17:37:19 2012 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Fri Sep 14 18:12:41 2012 +0200
@@ -171,7 +171,7 @@
private var control: Boolean = false
- private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.subexp _)
+ private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.highlight _)
def highlight_info(): Option[Text.Info[Color]] = highlight_area.info
private val hyperlink_area = new Active_Area[Hyperlink]((r: Isabelle_Rendering) => r.hyperlink _)
--- a/src/Tools/jEdit/src/isabelle_rendering.scala Fri Sep 14 17:37:19 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala Fri Sep 14 18:12:41 2012 +0200
@@ -97,9 +97,9 @@
val error_color = color_value("error_color")
val error1_color = color_value("error1_color")
val bad_color = color_value("bad_color")
- val hilite_color = color_value("hilite_color")
+ val intensify_color = color_value("intensify_color")
val quoted_color = color_value("quoted_color")
- val subexp_color = color_value("subexp_color")
+ val highlight_color = color_value("highlight_color")
val hyperlink_color = color_value("hyperlink_color")
val keyword1_color = color_value("keyword1_color")
val keyword2_color = color_value("keyword2_color")
@@ -154,19 +154,19 @@
/* markup selectors */
- private val subexp_include =
+ private val highlight_include =
Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP,
Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
Isabelle_Markup.PATH, Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM,
Isabelle_Markup.BOUND, Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR,
Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOCUMENT_SOURCE)
- def subexp(range: Text.Range): Option[Text.Info[Color]] =
+ def highlight(range: Text.Range): Option[Text.Info[Color]] =
{
- snapshot.select_markup(range, Some(subexp_include),
+ snapshot.select_markup(range, Some(highlight_include),
{
- case Text.Info(info_range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
- Text.Info(snapshot.convert(info_range), subexp_color)
+ case Text.Info(info_range, XML.Elem(Markup(name, _), _)) if highlight_include(name) =>
+ Text.Info(snapshot.convert(info_range), highlight_color)
}) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
}
@@ -346,15 +346,15 @@
Text.Info(r, result) <-
snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
range, (Some(Protocol.Status.init), None),
- Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.HILITE),
+ Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.INTENSIFY),
{
case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
if (Protocol.command_status_markup(markup.name)) =>
(Some(Protocol.command_status(status, markup)), color)
case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) =>
(None, Some(bad_color))
- case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _))) =>
- (None, Some(hilite_color))
+ case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.INTENSIFY, _), _))) =>
+ (None, Some(intensify_color))
})
color <-
(result match {
--- a/src/Tools/quickcheck.ML Fri Sep 14 17:37:19 2012 +0200
+++ b/src/Tools/quickcheck.ML Fri Sep 14 18:12:41 2012 +0200
@@ -529,7 +529,7 @@
state
|> (if auto then
Proof.goal_message (K (Pretty.chunks [Pretty.str "",
- Pretty.mark Isabelle_Markup.hilite msg]))
+ Pretty.mark Isabelle_Markup.intensify msg]))
else
tap (fn _ => Output.urgent_message (Pretty.string_of msg))))
else
--- a/src/Tools/solve_direct.ML Fri Sep 14 17:37:19 2012 +0200
+++ b/src/Tools/solve_direct.ML Fri Sep 14 18:12:41 2012 +0200
@@ -89,7 +89,7 @@
Proof.goal_message
(fn () =>
Pretty.chunks
- [Pretty.str "", Pretty.markup Isabelle_Markup.hilite (message results)])
+ [Pretty.str "", Pretty.markup Isabelle_Markup.intensify (message results)])
else
tap (fn _ =>
Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))