tuned;
authorwenzelm
Sat Aug 13 13:48:26 2011 +0200 (2011-08-13)
changeset 44181bbce0417236d
parent 44180 a6dc270d3edb
child 44182 ecb51b457064
tuned;
src/Pure/General/symbol.scala
src/Pure/General/yxml.scala
src/Pure/Isar/parse.scala
src/Tools/jEdit/src/isabelle_markup.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
     1.1 --- a/src/Pure/General/symbol.scala	Sat Aug 13 13:42:35 2011 +0200
     1.2 +++ b/src/Pure/General/symbol.scala	Sat Aug 13 13:48:26 2011 +0200
     1.3 @@ -179,7 +179,7 @@
     1.4          tab.get(x) match {
     1.5            case None => tab += (x -> y)
     1.6            case Some(z) =>
     1.7 -            error("Duplicate mapping of \"" + x + "\" to \"" + y + "\" vs. \"" + z + "\"")
     1.8 +            error("Duplicate mapping of " + quote(x) + " to " + quote(y) + " vs. " + quote(z))
     1.9          }
    1.10        }
    1.11        tab
     2.1 --- a/src/Pure/General/yxml.scala	Sat Aug 13 13:42:35 2011 +0200
     2.2 +++ b/src/Pure/General/yxml.scala	Sat Aug 13 13:48:26 2011 +0200
     2.3 @@ -50,7 +50,7 @@
     2.4    private def err_element() = err("bad element")
     2.5    private def err_unbalanced(name: String) =
     2.6      if (name == "") err("unbalanced element")
     2.7 -    else err("unbalanced element \"" + name + "\"")
     2.8 +    else err("unbalanced element " + quote(name))
     2.9  
    2.10    private def parse_attrib(source: CharSequence) = {
    2.11      val s = source.toString
     3.1 --- a/src/Pure/Isar/parse.scala	Sat Aug 13 13:42:35 2011 +0200
     3.2 +++ b/src/Pure/Isar/parse.scala	Sat Aug 13 13:48:26 2011 +0200
     3.3 @@ -50,7 +50,7 @@
     3.4        token(s, pred) ^^ (_.content)
     3.5  
     3.6      def keyword(name: String): Parser[String] =
     3.7 -      atom(Token.Kind.KEYWORD.toString + " \"" + name + "\"",
     3.8 +      atom(Token.Kind.KEYWORD.toString + " " + quote(name),
     3.9          tok => tok.kind == Token.Kind.KEYWORD && tok.content == name)
    3.10  
    3.11      def name: Parser[String] = atom("name declaration", _.is_name)
     4.1 --- a/src/Tools/jEdit/src/isabelle_markup.scala	Sat Aug 13 13:42:35 2011 +0200
     4.2 +++ b/src/Tools/jEdit/src/isabelle_markup.scala	Sat Aug 13 13:48:26 2011 +0200
     4.3 @@ -165,7 +165,7 @@
     4.4  
     4.5    val tooltip: Markup_Tree.Select[String] =
     4.6    {
     4.7 -    case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " \"" + name + "\""
     4.8 +    case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name)
     4.9      case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
    4.10        Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)),
    4.11          margin = Isabelle.Int_Property("tooltip-margin"))
     5.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Aug 13 13:42:35 2011 +0200
     5.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Aug 13 13:48:26 2011 +0200
     5.3 @@ -167,7 +167,7 @@
     5.4                new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
     5.5                  override def getShortString: String = content
     5.6                  override def getLongString: String = info_text
     5.7 -                override def toString = "\"" + content + "\" " + range.toString
     5.8 +                override def toString = quote(content) + " " + range.toString
     5.9                })
    5.10            })
    5.11      }