--- a/src/Pure/General/symbol_pos.ML Fri Jan 12 20:19:59 2018 +0100
+++ b/src/Pure/General/symbol_pos.ML Sat Jan 13 11:22:46 2018 +0100
@@ -34,6 +34,8 @@
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
@@ -216,10 +218,18 @@
val recover_cartouche = Scan.pass (SOME 0) scan_cartouche_depth;
-fun scan_comment_cartouche err_prefix =
- $$$ Symbol.comment @@@ Scan.many (Symbol.is_blank o symbol) @@@
- !!! (fn () => err_prefix ^ "cartouche expected after " ^ quote Symbol.comment)
- (scan_cartouche err_prefix);
+
+(* 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 *)