# HG changeset patch
# User wenzelm
# Date 1515938787 -3600
# Node ID 6311cf9dc943cc1cada8d9645f2a51b246b9ddc4
# Parent  7d4a088dbc0e6a710666155d8e16a5c90eeceb9b
clarified signature;

diff -r 7d4a088dbc0e -r 6311cf9dc943 src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Sun Jan 14 14:11:02 2018 +0100
+++ b/src/Pure/General/antiquote.ML	Sun Jan 14 15:06:27 2018 +0100
@@ -13,9 +13,9 @@
   val range: text_antiquote list -> Position.range
   val split_lines: text_antiquote list -> text_antiquote list list
   val antiq_reports: 'a antiquote list -> Position.report list
-  val scan_control: Symbol_Pos.T list -> control * Symbol_Pos.T list
-  val scan_antiq: Symbol_Pos.T list -> antiq * Symbol_Pos.T list
-  val scan_antiquote: Symbol_Pos.T list -> text_antiquote * Symbol_Pos.T list
+  val scan_control: control scanner
+  val scan_antiq: antiq scanner
+  val scan_antiquote: text_antiquote scanner
   val parse: Position.T -> Symbol_Pos.T list -> text_antiquote list
   val read: Input.source -> text_antiquote list
 end;
diff -r 7d4a088dbc0e -r 6311cf9dc943 src/Pure/General/comment.ML
--- a/src/Pure/General/comment.ML	Sun Jan 14 14:11:02 2018 +0100
+++ b/src/Pure/General/comment.ML	Sun Jan 14 15:06:27 2018 +0100
@@ -7,9 +7,9 @@
 signature COMMENT =
 sig
   datatype kind = Comment | Cancel
-  val scan_comment: Symbol_Pos.T list -> (kind * Symbol_Pos.T list) * Symbol_Pos.T list
-  val scan_cancel: Symbol_Pos.T list -> (kind * Symbol_Pos.T list) * Symbol_Pos.T list
-  val scan: Symbol_Pos.T list -> (kind * Symbol_Pos.T list) * Symbol_Pos.T list
+  val scan_comment: (kind * Symbol_Pos.T list) scanner
+  val scan_cancel: (kind * Symbol_Pos.T list) scanner
+  val scan: (kind * Symbol_Pos.T list) scanner
   val read_body: Symbol_Pos.T list -> (kind option * Symbol_Pos.T list) list option
 end;
 
diff -r 7d4a088dbc0e -r 6311cf9dc943 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Sun Jan 14 14:11:02 2018 +0100
+++ b/src/Pure/General/symbol_pos.ML	Sun Jan 14 15:06:27 2018 +0100
@@ -7,11 +7,8 @@
 signature SYMBOL_POS =
 sig
   type T = Symbol.symbol * Position.T
+  type 'a scanner = T list -> 'a * T list
   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
   val range: T list -> Position.range
   val split_lines: T list -> T list list
@@ -19,24 +16,28 @@
   val trim_lines: T list -> T list
   val is_eof: T -> bool
   val stopper: T Scan.stopper
-  val !!! : Scan.message -> (T list -> 'a) -> T list -> 'a
-  val scan_pos: T list -> Position.T * T list
-  val scan_string_q: string -> T list -> (Position.T * (T list * Position.T)) * T list
-  val scan_string_qq: string -> T list -> (Position.T * (T list * Position.T)) * T list
-  val scan_string_bq: string -> T list -> (Position.T * (T list * Position.T)) * T list
-  val recover_string_q: T list -> T list * T list
-  val recover_string_qq: T list -> T list * T list
-  val recover_string_bq: T list -> T list * T list
+  val !!! : Scan.message -> 'a scanner -> 'a scanner
+  val $$ : Symbol.symbol -> T scanner
+  val ~$$ : Symbol.symbol -> T scanner
+  val $$$ : Symbol.symbol -> T list scanner
+  val ~$$$ : Symbol.symbol -> T list scanner
+  val scan_pos: Position.T scanner
+  val scan_string_q: string -> (Position.T * (T list * Position.T)) scanner
+  val scan_string_qq: string -> (Position.T * (T list * Position.T)) scanner
+  val scan_string_bq: string -> (Position.T * (T list * Position.T)) scanner
+  val recover_string_q: T list scanner
+  val recover_string_qq: T list scanner
+  val recover_string_bq: T list scanner
   val quote_string_q: string -> string
   val quote_string_qq: string -> string
   val quote_string_bq: string -> string
   val cartouche_content: T list -> T list
-  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_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
+  val scan_cartouche: string -> T list scanner
+  val scan_cartouche_content: string -> T list scanner
+  val recover_cartouche: T list scanner
+  val scan_comment: string -> T list scanner
+  val scan_comment_body: string -> T list scanner
+  val recover_comment: T list scanner
   val source: Position.T -> (Symbol.symbol, 'a) Source.source ->
     (T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source
   type text = string
@@ -44,10 +45,10 @@
   val implode_range: Position.range -> T list -> text * Position.range
   val explode: text * Position.T -> T list
   val explode0: string -> T list
-  val scan_ident: T list -> T list * T list
+  val scan_ident: T list scanner
   val is_identifier: string -> bool
-  val scan_nat: T list -> T list * T list
-  val scan_float: T list -> T list * T list
+  val scan_nat: T list scanner
+  val scan_float: T list scanner
 end;
 
 structure Symbol_Pos: SYMBOL_POS =
@@ -56,6 +57,7 @@
 (* type T *)
 
 type T = Symbol.symbol * Position.T;
+type 'a scanner = T list -> 'a * T list;
 
 fun symbol ((s, _): T) = s;
 
@@ -97,7 +99,7 @@
 
 (* basic scanners *)
 
-fun !!! text scan =
+fun !!! text (scan: 'a scanner) =
   let
     fun get_pos [] = " (end-of-input)"
       | get_pos ((_, pos) :: _) = Position.here pos;
@@ -317,3 +319,5 @@
   val $$$ = Symbol_Pos.$$$;
   val ~$$$ = Symbol_Pos.~$$$;
 end;
+
+type 'a scanner = 'a Symbol_Pos.scanner;
diff -r 7d4a088dbc0e -r 6311cf9dc943 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Sun Jan 14 14:11:02 2018 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Sun Jan 14 15:06:27 2018 +0100
@@ -12,13 +12,13 @@
     val free: string -> term
     val var: indexname -> term
   end
-  val scan_id: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
-  val scan_longid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
-  val scan_tid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
-  val scan_hex: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
-  val scan_bin: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
-  val scan_var: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
-  val scan_tvar: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
+  val scan_id: Symbol_Pos.T list scanner
+  val scan_longid: Symbol_Pos.T list scanner
+  val scan_tid: Symbol_Pos.T list scanner
+  val scan_hex: Symbol_Pos.T list scanner
+  val scan_bin: Symbol_Pos.T list scanner
+  val scan_var: Symbol_Pos.T list scanner
+  val scan_tvar: Symbol_Pos.T list scanner
   val is_tid: string -> bool
   datatype token_kind =
     Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy | FloatSy |