# HG changeset patch # User wenzelm # Date 1347639161 -7200 # Node ID 0fa351b1bd14b075e54befdc2e30de09fcc5773c # Parent 34ac36642a3136833acf18d2f784c5e9df18ae01 clarified markup names; diff -r 34ac36642a31 -r 0fa351b1bd14 src/HOL/Tools/Nitpick/nitpick.ML --- 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 diff -r 34ac36642a31 -r 0fa351b1bd14 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- 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 diff -r 34ac36642a31 -r 0fa351b1bd14 src/HOL/Tools/try0.ML --- 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)))) diff -r 34ac36642a31 -r 0fa351b1bd14 src/Pure/General/name_space.ML --- 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); diff -r 34ac36642a31 -r 0fa351b1bd14 src/Pure/PIDE/isabelle_markup.ML --- 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 *) diff -r 34ac36642a31 -r 0fa351b1bd14 src/Pure/PIDE/isabelle_markup.scala --- 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 */ diff -r 34ac36642a31 -r 0fa351b1bd14 src/Pure/ProofGeneral/proof_general_emacs.ML --- 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") diff -r 34ac36642a31 -r 0fa351b1bd14 src/Pure/Syntax/syntax_phases.ML --- 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) diff -r 34ac36642a31 -r 0fa351b1bd14 src/Tools/jEdit/etc/isabelle-jedit.css --- 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; } diff -r 34ac36642a31 -r 0fa351b1bd14 src/Tools/jEdit/etc/options --- 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" diff -r 34ac36642a31 -r 0fa351b1bd14 src/Tools/jEdit/src/document_view.scala --- 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 _) diff -r 34ac36642a31 -r 0fa351b1bd14 src/Tools/jEdit/src/isabelle_rendering.scala --- 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 { diff -r 34ac36642a31 -r 0fa351b1bd14 src/Tools/quickcheck.ML --- 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 diff -r 34ac36642a31 -r 0fa351b1bd14 src/Tools/solve_direct.ML --- 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))))))