# HG changeset patch
# User wenzelm
# Date 1445181620 -7200
# Node ID c42960228a81796a8683b33143e1920fa165dcfb
# Parent  7d1127ac2251c5082ac5ab2533a101181b2b41ed
clarified Symbol.is_control;

diff -r 7d1127ac2251 -r c42960228a81 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Sat Oct 17 16:08:30 2015 +0200
+++ b/src/Pure/General/symbol.ML	Sun Oct 18 17:20:20 2015 +0200
@@ -15,6 +15,7 @@
   val is_symbolic: symbol -> bool
   val is_symbolic_char: symbol -> bool
   val is_printable: symbol -> bool
+  val is_control: symbol -> bool
   val eof: symbol
   val is_eof: symbol -> bool
   val not_eof: symbol -> bool
@@ -108,6 +109,9 @@
   if is_char s then ord space <= ord s andalso ord s <= ord "~"
   else is_utf8 s orelse raw_symbolic s;
 
+fun is_control s =
+  String.isPrefix "\\<^" s andalso String.isSuffix ">" s;
+
 
 (* input source control *)
 
@@ -228,7 +232,7 @@
   else if is_utf8 s then UTF8 s
   else if is_raw s then Raw (decode_raw s)
   else if is_malformed s then Malformed s
-  else if String.isPrefix "\\<^" s then Ctrl (String.substring (s, 3, size s - 4))
+  else if is_control s then Ctrl (String.substring (s, 3, size s - 4))
   else Sym (String.substring (s, 2, size s - 3));
 
 
diff -r 7d1127ac2251 -r c42960228a81 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Sat Oct 17 16:08:30 2015 +0200
+++ b/src/Pure/General/symbol.scala	Sun Oct 18 17:20:20 2015 +0200
@@ -521,7 +521,7 @@
   /* control symbols */
 
   def is_control(sym: Symbol): Boolean =
-    sym.startsWith("\\<^") || symbols.control_decoded.contains(sym)
+    (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)
diff -r 7d1127ac2251 -r c42960228a81 src/Pure/Thy/term_style.ML
--- a/src/Pure/Thy/term_style.ML	Sat Oct 17 16:08:30 2015 +0200
+++ b/src/Pure/Thy/term_style.ML	Sun Oct 18 17:20:20 2015 +0200
@@ -67,7 +67,7 @@
   end);
 
 fun sub_symbols (d :: s :: ss) =
-      if Symbol.is_ascii_digit d andalso not (String.isPrefix ("\<^") s)
+      if Symbol.is_ascii_digit d andalso not (Symbol.is_control s)
       then d :: "\<^sub>" :: sub_symbols (s :: ss)
       else d :: s :: ss
   | sub_symbols cs = cs;