# HG changeset patch
# User wenzelm
# Date 1496661554 -7200
# Node ID cec184536dfdd10ad5f3e805dddce0a30fe09329
# Parent  10e5265c2a25ae4c15190621077d5c4cf65bb1ec
uniform notion of Symbol.is_controllable (see also 265d9300d523);

diff -r 10e5265c2a25 -r cec184536dfd src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Fri Jun 02 09:26:04 2017 +0200
+++ b/src/Pure/General/symbol.scala	Mon Jun 05 13:19:14 2017 +0200
@@ -579,7 +579,8 @@
     (sym.startsWith("\\<^") && sym.endsWith(">")) || symbols.control_decoded.contains(sym)
 
   def is_controllable(sym: Symbol): Boolean =
-    !is_blank(sym) && !is_control(sym) && !is_open(sym) && !is_close(sym) && !is_malformed(sym)
+    !is_blank(sym) && !is_control(sym) && !is_open(sym) && !is_close(sym) &&
+    !is_malformed(sym) && sym != "\""
 
   val sub = "\\<^sub>"
   val sup = "\\<^sup>"
diff -r 10e5265c2a25 -r cec184536dfd src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Fri Jun 02 09:26:04 2017 +0200
+++ b/src/Pure/Thy/html.scala	Mon Jun 05 13:19:14 2017 +0200
@@ -48,7 +48,7 @@
       if (is_control(sym)) { output_symbol(ctrl); ctrl = sym }
       else {
         control.get(ctrl) match {
-          case Some(elem) if Symbol.is_controllable(sym) && sym != "\"" =>
+          case Some(elem) if Symbol.is_controllable(sym) =>
             output_hidden(output_symbol(ctrl))
             s += '<'; s ++= elem; s += '>'
             output_symbol(sym)
diff -r 10e5265c2a25 -r cec184536dfd src/Tools/jEdit/src/syntax_style.scala
--- a/src/Tools/jEdit/src/syntax_style.scala	Fri Jun 02 09:26:04 2017 +0200
+++ b/src/Tools/jEdit/src/syntax_style.scala	Mon Jun 05 13:19:14 2017 +0200
@@ -109,7 +109,7 @@
     for (sym <- Symbol.iterator(text)) {
       if (control_style(sym).isDefined) control = sym
       else if (control != "") {
-        if (Symbol.is_controllable(sym) && sym != "\"" && !Symbol.fonts.isDefinedAt(sym)) {
+        if (Symbol.is_controllable(sym) && !Symbol.fonts.isDefinedAt(sym)) {
           mark(offset - control.length, offset, _ => hidden)
           mark(offset, offset + sym.length, control_style(control).get)
         }