tuned signature;

--- a/src/Pure/General/antiquote.ML	Mon Jan 20 20:24:44 2014 +0100
+++ b/src/Pure/General/antiquote.ML	Mon Jan 20 20:38:51 2014 +0100
@@ -45,7 +45,7 @@
 val err_prefix = "Antiquotation lexical error: ";
 
 val scan_txt =
-  $$$ "@" --| Scan.ahead (~$$$ "{") ||
+  $$$ "@" --| Scan.ahead (~$$ "{") ||
   Scan.one (fn (s, _) => s <> "@" andalso Symbol.is_regular s) >> single;
 
 val scan_ant =
@@ -56,9 +56,9 @@
 in
 
 val scan_antiq =
-  Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
+  Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |--
     Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace")
-      (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
+      (Scan.repeat scan_ant -- ($$ "}" |-- Symbol_Pos.scan_pos)))
   >> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2));
 
 val scan_text = scan_antiq >> Antiq || Scan.repeat1 scan_txt >> (Text o flat);

--- a/src/Pure/General/symbol_pos.ML	Mon Jan 20 20:24:44 2014 +0100
+++ b/src/Pure/General/symbol_pos.ML	Mon Jan 20 20:38:51 2014 +0100
@@ -9,6 +9,7 @@
   type T = Symbol.symbol * Position.T
   val symbol: T -> Symbol.symbol
   val $$ : Symbol.symbol -> T list -> T * T list
+  val ~$$ : Symbol.symbol -> T list -> T * T list
   val $$$ : Symbol.symbol -> T list -> T list * T list
   val ~$$$ : Symbol.symbol -> T list -> T list * T list
   val content: T list -> string
@@ -87,6 +88,8 @@
 fun change_prompt scan = Scan.prompt "# " scan;
 
 fun $$ s = Scan.one (fn x => symbol x = s);
+fun ~$$ s = Scan.one (fn x => symbol x <> s);
+
 fun $$$ s = Scan.one (fn x => symbol x = s) >> single;
 fun ~$$$ s = Scan.one (fn x => symbol x <> s) >> single;
 
@@ -278,6 +281,7 @@
 structure Basic_Symbol_Pos =   (*not open by default*)
 struct
   val $$ = Symbol_Pos.$$;
+  val ~$$ = Symbol_Pos.~$$;
   val $$$ = Symbol_Pos.$$$;
   val ~$$$ = Symbol_Pos.~$$$;
 end;

--- a/src/Pure/Isar/token.ML	Mon Jan 20 20:24:44 2014 +0100
+++ b/src/Pure/Isar/token.ML	Mon Jan 20 20:38:51 2014 +0100
@@ -321,15 +321,15 @@
 (* scan verbatim text *)
 
 val scan_verb =
-  $$$ "*" --| Scan.ahead (~$$$ "}") ||
+  $$$ "*" --| Scan.ahead (~$$ "}") ||
   Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single;
 
 val scan_verbatim =
-  Scan.ahead ($$$ "{" -- $$$ "*") |--
+  Scan.ahead ($$ "{" -- $$ "*") |--
     !!! "unclosed verbatim text"
-      ((Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") --
+      ((Symbol_Pos.scan_pos --| $$ "{" --| $$ "*") --
         Symbol_Pos.change_prompt
-          ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
+          ((Scan.repeat scan_verb >> flat) -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos)));
 
 val recover_verbatim =
   $$$ "{" @@@ $$$ "*" @@@ (Scan.repeat scan_verb >> flat);

--- a/src/Pure/Syntax/lexicon.ML	Mon Jan 20 20:24:44 2014 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Mon Jan 20 20:38:51 2014 +0100
@@ -210,11 +210,11 @@
 (* str tokens *)
 
 val scan_chr =
-  $$$ "\\" |-- $$$ "'" ||
+  $$ "\\" |-- $$$ "'" ||
   Scan.one
     ((fn s => s <> "\\" andalso s <> "'" andalso Symbol.is_regular s) o
       Symbol_Pos.symbol) >> single ||
-  $$$ "'" --| Scan.ahead (~$$$ "'");
+  $$$ "'" --| Scan.ahead (~$$ "'");
 
 val scan_str =
   Scan.ahead ($$ "'" -- $$ "'") |--
@@ -222,7 +222,7 @@
       ($$$ "'" @@@ $$$ "'" @@@ (Scan.repeat scan_chr >> flat) @@@ $$$ "'" @@@ $$$ "'");
 
 val scan_str_body =
-  Scan.ahead ($$$ "'" |-- $$$ "'") |--
+  Scan.ahead ($$ "'" |-- $$ "'") |--
     !!! "unclosed string literal"
       ($$ "'" |-- $$ "'" |-- (Scan.repeat scan_chr >> flat) --| $$ "'" --| $$ "'");
 
@@ -297,7 +297,7 @@
 
     val scan =
       (scan_id >> map Symbol_Pos.symbol) --
-      Scan.optional ($$$ "." |-- scan_nat >> (nat 0 o map Symbol_Pos.symbol)) ~1;
+      Scan.optional ($$ "." |-- scan_nat >> (nat 0 o map Symbol_Pos.symbol)) ~1;
   in
     scan >>
       (fn (cs, ~1) => chop_idx (rev cs) []
@@ -306,7 +306,7 @@
 
 in
 
-val scan_indexname = $$$ "'" |-- scan_vname >> (fn (x, i) => ("'" ^ x, i)) || scan_vname;
+val scan_indexname = $$ "'" |-- scan_vname >> (fn (x, i) => ("'" ^ x, i)) || scan_vname;
 
 end;
 
@@ -324,7 +324,7 @@
 fun read_var str =
   let
     val scan =
-      $$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof)
+      $$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof)
         >> Syntax.var ||
       Scan.many (Symbol.is_regular o Symbol_Pos.symbol)
         >> (Syntax.free o implode o map Symbol_Pos.symbol);
@@ -334,7 +334,7 @@
 (* read_variable *)
 
 fun read_variable str =
-  let val scan = $$$ "?" |-- scan_indexname || scan_indexname
+  let val scan = $$ "?" |-- scan_indexname || scan_indexname
   in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none)) end;