clarified markup names;
authorwenzelm
Fri Sep 14 18:12:41 2012 +0200 (2012-09-14 ago)
changeset 493580fa351b1bd14
parent 49357 34ac36642a31
child 49359 c1262d7389fb
clarified markup names;
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
src/HOL/Tools/try0.ML
src/Pure/General/name_space.ML
src/Pure/PIDE/isabelle_markup.ML
src/Pure/PIDE/isabelle_markup.scala
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/Syntax/syntax_phases.ML
src/Tools/jEdit/etc/isabelle-jedit.css
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/isabelle_rendering.scala
src/Tools/quickcheck.ML
src/Tools/solve_direct.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri Sep 14 17:37:19 2012 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Sep 14 18:12:41 2012 +0200
     1.3 @@ -245,7 +245,7 @@
     1.4        if mode = Auto_Try then
     1.5          Unsynchronized.change state_ref o Proof.goal_message o K
     1.6          o Pretty.chunks o cons (Pretty.str "") o single
     1.7 -        o Pretty.mark Isabelle_Markup.hilite
     1.8 +        o Pretty.mark Isabelle_Markup.intensify
     1.9        else
    1.10          print o Pretty.string_of
    1.11      val pprint_a = pprint Output.urgent_message
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Sep 14 17:37:19 2012 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Sep 14 18:12:41 2012 +0200
     2.3 @@ -137,7 +137,7 @@
     2.4           |> outcome_code = someN
     2.5              ? Proof.goal_message (fn () =>
     2.6                    [Pretty.str "",
     2.7 -                   Pretty.mark Isabelle_Markup.hilite (Pretty.str (message ()))]
     2.8 +                   Pretty.mark Isabelle_Markup.intensify (Pretty.str (message ()))]
     2.9                    |> Pretty.chunks))
    2.10        end
    2.11      else if blocking then
     3.1 --- a/src/HOL/Tools/try0.ML	Fri Sep 14 17:37:19 2012 +0200
     3.2 +++ b/src/HOL/Tools/try0.ML	Fri Sep 14 18:12:41 2012 +0200
     3.3 @@ -146,7 +146,7 @@
     3.4          (true, (s, st |> (if mode = Auto_Try then
     3.5                              Proof.goal_message
     3.6                                  (fn () => Pretty.chunks [Pretty.str "",
     3.7 -                                          Pretty.markup Isabelle_Markup.hilite
     3.8 +                                          Pretty.markup Isabelle_Markup.intensify
     3.9                                                          [Pretty.str message]])
    3.10                            else
    3.11                              tap (fn _ => Output.urgent_message message))))
     4.1 --- a/src/Pure/General/name_space.ML	Fri Sep 14 17:37:19 2012 +0200
     4.2 +++ b/src/Pure/General/name_space.ML	Fri Sep 14 18:12:41 2012 +0200
     4.3 @@ -133,7 +133,7 @@
     4.4  
     4.5  fun markup (Name_Space {kind, entries, ...}) name =
     4.6    (case Symtab.lookup entries name of
     4.7 -    NONE => Isabelle_Markup.hilite
     4.8 +    NONE => Isabelle_Markup.intensify
     4.9    | SOME (_, entry) => entry_markup false kind (name, entry));
    4.10  
    4.11  fun is_concealed space name = #concealed (the_entry space name);
     5.1 --- a/src/Pure/PIDE/isabelle_markup.ML	Fri Sep 14 17:37:19 2012 +0200
     5.2 +++ b/src/Pure/PIDE/isabelle_markup.ML	Fri Sep 14 18:12:41 2012 +0200
     5.3 @@ -84,7 +84,7 @@
     5.4    val stateN: string val state: Markup.T
     5.5    val subgoalN: string val subgoal: Markup.T
     5.6    val sendbackN: string val sendback: Markup.T
     5.7 -  val hiliteN: string val hilite: Markup.T
     5.8 +  val intensifyN: string val intensify: Markup.T
     5.9    val taskN: string
    5.10    val acceptedN: string val accepted: Markup.T
    5.11    val forkedN: string val forked: Markup.T
    5.12 @@ -264,7 +264,7 @@
    5.13  val (stateN, state) = markup_elem "state";
    5.14  val (subgoalN, subgoal) = markup_elem "subgoal";
    5.15  val (sendbackN, sendback) = markup_elem "sendback";
    5.16 -val (hiliteN, hilite) = markup_elem "hilite";
    5.17 +val (intensifyN, intensify) = markup_elem "intensify";
    5.18  
    5.19  
    5.20  (* command status *)
     6.1 --- a/src/Pure/PIDE/isabelle_markup.scala	Fri Sep 14 17:37:19 2012 +0200
     6.2 +++ b/src/Pure/PIDE/isabelle_markup.scala	Fri Sep 14 18:12:41 2012 +0200
     6.3 @@ -185,7 +185,7 @@
     6.4    val STATE = "state"
     6.5    val SUBGOAL = "subgoal"
     6.6    val SENDBACK = "sendback"
     6.7 -  val HILITE = "hilite"
     6.8 +  val INTENSIFY = "intensify"
     6.9  
    6.10  
    6.11    /* command status */
     7.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Sep 14 17:37:19 2012 +0200
     7.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Sep 14 18:12:41 2012 +0200
     7.3 @@ -41,7 +41,7 @@
     7.4            if null ts then Markup.no_output
     7.5            else if name = Isabelle_Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
     7.6            else if name = Isabelle_Markup.sendbackN then (special "W", special "X")
     7.7 -          else if name = Isabelle_Markup.hiliteN then (special "0", special "1")
     7.8 +          else if name = Isabelle_Markup.intensifyN then (special "0", special "1")
     7.9            else if name = Isabelle_Markup.tfreeN then (special "C", special "A")
    7.10            else if name = Isabelle_Markup.tvarN then (special "D", special "A")
    7.11            else if name = Isabelle_Markup.freeN then (special "E", special "A")
     8.1 --- a/src/Pure/Syntax/syntax_phases.ML	Fri Sep 14 17:37:19 2012 +0200
     8.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Fri Sep 14 18:12:41 2012 +0200
     8.3 @@ -586,7 +586,7 @@
     8.4      val m =
     8.5        if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt
     8.6        then Isabelle_Markup.fixed x
     8.7 -      else Isabelle_Markup.hilite;
     8.8 +      else Isabelle_Markup.intensify;
     8.9    in
    8.10      if can Name.dest_skolem x
    8.11      then ([m, Isabelle_Markup.skolem], Variable.revert_fixed ctxt x)
     9.1 --- a/src/Tools/jEdit/etc/isabelle-jedit.css	Fri Sep 14 17:37:19 2012 +0200
     9.2 +++ b/src/Tools/jEdit/etc/isabelle-jedit.css	Fri Sep 14 18:12:41 2012 +0200
     9.3 @@ -9,7 +9,7 @@
     9.4  
     9.5  .report { display: none; }
     9.6  
     9.7 -.hilite { background-color: #FFCC66; }
     9.8 +.intensify { background-color: #FFCC66; }
     9.9  
    9.10  .keyword { font-weight: bold; color: #009966; }
    9.11  .operator { font-weight: bold; }
    10.1 --- a/src/Tools/jEdit/etc/options	Fri Sep 14 17:37:19 2012 +0200
    10.2 +++ b/src/Tools/jEdit/etc/options	Fri Sep 14 18:12:41 2012 +0200
    10.3 @@ -32,9 +32,9 @@
    10.4  option error_color : string = "B22222FF"
    10.5  option error1_color : string = "B2222232"
    10.6  option bad_color : string = "FF6A6A64"
    10.7 -option hilite_color : string = "FFCC6664"
    10.8 +option intensify_color : string = "FFCC6664"
    10.9  option quoted_color : string = "8B8B8B19"
   10.10 -option subexp_color : string = "50505032"
   10.11 +option highlight_color : string = "50505032"
   10.12  option hyperlink_color : string = "000000FF"
   10.13  option keyword1_color : string = "006699FF"
   10.14  option keyword2_color : string = "009966FF"
    11.1 --- a/src/Tools/jEdit/src/document_view.scala	Fri Sep 14 17:37:19 2012 +0200
    11.2 +++ b/src/Tools/jEdit/src/document_view.scala	Fri Sep 14 18:12:41 2012 +0200
    11.3 @@ -171,7 +171,7 @@
    11.4  
    11.5    private var control: Boolean = false
    11.6  
    11.7 -  private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.subexp _)
    11.8 +  private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.highlight _)
    11.9    def highlight_info(): Option[Text.Info[Color]] = highlight_area.info
   11.10  
   11.11    private val hyperlink_area = new Active_Area[Hyperlink]((r: Isabelle_Rendering) => r.hyperlink _)
    12.1 --- a/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Sep 14 17:37:19 2012 +0200
    12.2 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Sep 14 18:12:41 2012 +0200
    12.3 @@ -97,9 +97,9 @@
    12.4    val error_color = color_value("error_color")
    12.5    val error1_color = color_value("error1_color")
    12.6    val bad_color = color_value("bad_color")
    12.7 -  val hilite_color = color_value("hilite_color")
    12.8 +  val intensify_color = color_value("intensify_color")
    12.9    val quoted_color = color_value("quoted_color")
   12.10 -  val subexp_color = color_value("subexp_color")
   12.11 +  val highlight_color = color_value("highlight_color")
   12.12    val hyperlink_color = color_value("hyperlink_color")
   12.13    val keyword1_color = color_value("keyword1_color")
   12.14    val keyword2_color = color_value("keyword2_color")
   12.15 @@ -154,19 +154,19 @@
   12.16  
   12.17    /* markup selectors */
   12.18  
   12.19 -  private val subexp_include =
   12.20 +  private val highlight_include =
   12.21      Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP,
   12.22        Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
   12.23        Isabelle_Markup.PATH, Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM,
   12.24        Isabelle_Markup.BOUND, Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR,
   12.25        Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOCUMENT_SOURCE)
   12.26  
   12.27 -  def subexp(range: Text.Range): Option[Text.Info[Color]] =
   12.28 +  def highlight(range: Text.Range): Option[Text.Info[Color]] =
   12.29    {
   12.30 -    snapshot.select_markup(range, Some(subexp_include),
   12.31 +    snapshot.select_markup(range, Some(highlight_include),
   12.32          {
   12.33 -          case Text.Info(info_range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
   12.34 -            Text.Info(snapshot.convert(info_range), subexp_color)
   12.35 +          case Text.Info(info_range, XML.Elem(Markup(name, _), _)) if highlight_include(name) =>
   12.36 +            Text.Info(snapshot.convert(info_range), highlight_color)
   12.37          }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
   12.38    }
   12.39  
   12.40 @@ -346,15 +346,15 @@
   12.41          Text.Info(r, result) <-
   12.42            snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
   12.43              range, (Some(Protocol.Status.init), None),
   12.44 -            Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.HILITE),
   12.45 +            Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.INTENSIFY),
   12.46              {
   12.47                case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
   12.48                if (Protocol.command_status_markup(markup.name)) =>
   12.49                  (Some(Protocol.command_status(status, markup)), color)
   12.50                case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) =>
   12.51                  (None, Some(bad_color))
   12.52 -              case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _))) =>
   12.53 -                (None, Some(hilite_color))
   12.54 +              case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.INTENSIFY, _), _))) =>
   12.55 +                (None, Some(intensify_color))
   12.56              })
   12.57          color <-
   12.58            (result match {
    13.1 --- a/src/Tools/quickcheck.ML	Fri Sep 14 17:37:19 2012 +0200
    13.2 +++ b/src/Tools/quickcheck.ML	Fri Sep 14 18:12:41 2012 +0200
    13.3 @@ -529,7 +529,7 @@
    13.4               state
    13.5               |> (if auto then
    13.6                     Proof.goal_message (K (Pretty.chunks [Pretty.str "",
    13.7 -                       Pretty.mark Isabelle_Markup.hilite msg]))
    13.8 +                       Pretty.mark Isabelle_Markup.intensify msg]))
    13.9                   else
   13.10                     tap (fn _ => Output.urgent_message (Pretty.string_of msg))))
   13.11            else
    14.1 --- a/src/Tools/solve_direct.ML	Fri Sep 14 17:37:19 2012 +0200
    14.2 +++ b/src/Tools/solve_direct.ML	Fri Sep 14 18:12:41 2012 +0200
    14.3 @@ -89,7 +89,7 @@
    14.4                 Proof.goal_message
    14.5                   (fn () =>
    14.6                     Pretty.chunks
    14.7 -                    [Pretty.str "", Pretty.markup Isabelle_Markup.hilite (message results)])
    14.8 +                    [Pretty.str "", Pretty.markup Isabelle_Markup.intensify (message results)])
    14.9               else
   14.10                 tap (fn _ =>
   14.11                   Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))