--- a/src/Pure/General/symbol_pos.ML Sat Jan 13 21:41:36 2018 +0100
+++ b/src/Pure/General/symbol_pos.ML Sun Jan 14 14:11:02 2018 +0100
@@ -34,9 +34,6 @@
val scan_cartouche: string -> T list -> T list * T list
val scan_cartouche_content: string -> T list -> T list * T list
val recover_cartouche: T list -> T list * T list
- val scan_blanks: T list -> T list * T list
- val scan_cancel_cartouche: string -> T list -> T list * T list
- val scan_comment_cartouche: string -> T list -> T list * T list
val scan_comment: string -> T list -> T list * T list
val scan_comment_body: string -> T list -> T list * T list
val recover_comment: T list -> T list * T list
@@ -219,19 +216,6 @@
val recover_cartouche = Scan.pass (SOME 0) scan_cartouche_depth;
-(* operator with cartouche argument *)
-
-val scan_blanks = Scan.many (Symbol.is_blank o symbol);
-
-fun scan_operator_cartouche blanks operator_symbol err_prefix =
- (if blanks then $$$ operator_symbol @@@ scan_blanks else $$$ operator_symbol) @@@
- !!! (fn () => err_prefix ^ "cartouche expected after " ^ quote operator_symbol)
- (scan_cartouche err_prefix);
-
-val scan_cancel_cartouche = scan_operator_cartouche false Symbol.cancel;
-val scan_comment_cartouche = scan_operator_cartouche true Symbol.comment;
-
-
(* ML-style comments *)
local