clarified signature;
authorwenzelm
Sun Jan 14 15:06:27 2018 +0100 (17 months ago)
changeset 674266311cf9dc943
parent 67425 7d4a088dbc0e
child 67427 5409cfd41e7f
clarified signature;
src/Pure/General/antiquote.ML
src/Pure/General/comment.ML
src/Pure/General/symbol_pos.ML
src/Pure/Syntax/lexicon.ML
     1.1 --- a/src/Pure/General/antiquote.ML	Sun Jan 14 14:11:02 2018 +0100
     1.2 +++ b/src/Pure/General/antiquote.ML	Sun Jan 14 15:06:27 2018 +0100
     1.3 @@ -13,9 +13,9 @@
     1.4    val range: text_antiquote list -> Position.range
     1.5    val split_lines: text_antiquote list -> text_antiquote list list
     1.6    val antiq_reports: 'a antiquote list -> Position.report list
     1.7 -  val scan_control: Symbol_Pos.T list -> control * Symbol_Pos.T list
     1.8 -  val scan_antiq: Symbol_Pos.T list -> antiq * Symbol_Pos.T list
     1.9 -  val scan_antiquote: Symbol_Pos.T list -> text_antiquote * Symbol_Pos.T list
    1.10 +  val scan_control: control scanner
    1.11 +  val scan_antiq: antiq scanner
    1.12 +  val scan_antiquote: text_antiquote scanner
    1.13    val parse: Position.T -> Symbol_Pos.T list -> text_antiquote list
    1.14    val read: Input.source -> text_antiquote list
    1.15  end;
     2.1 --- a/src/Pure/General/comment.ML	Sun Jan 14 14:11:02 2018 +0100
     2.2 +++ b/src/Pure/General/comment.ML	Sun Jan 14 15:06:27 2018 +0100
     2.3 @@ -7,9 +7,9 @@
     2.4  signature COMMENT =
     2.5  sig
     2.6    datatype kind = Comment | Cancel
     2.7 -  val scan_comment: Symbol_Pos.T list -> (kind * Symbol_Pos.T list) * Symbol_Pos.T list
     2.8 -  val scan_cancel: Symbol_Pos.T list -> (kind * Symbol_Pos.T list) * Symbol_Pos.T list
     2.9 -  val scan: Symbol_Pos.T list -> (kind * Symbol_Pos.T list) * Symbol_Pos.T list
    2.10 +  val scan_comment: (kind * Symbol_Pos.T list) scanner
    2.11 +  val scan_cancel: (kind * Symbol_Pos.T list) scanner
    2.12 +  val scan: (kind * Symbol_Pos.T list) scanner
    2.13    val read_body: Symbol_Pos.T list -> (kind option * Symbol_Pos.T list) list option
    2.14  end;
    2.15  
     3.1 --- a/src/Pure/General/symbol_pos.ML	Sun Jan 14 14:11:02 2018 +0100
     3.2 +++ b/src/Pure/General/symbol_pos.ML	Sun Jan 14 15:06:27 2018 +0100
     3.3 @@ -7,11 +7,8 @@
     3.4  signature SYMBOL_POS =
     3.5  sig
     3.6    type T = Symbol.symbol * Position.T
     3.7 +  type 'a scanner = T list -> 'a * T list
     3.8    val symbol: T -> Symbol.symbol
     3.9 -  val $$ : Symbol.symbol -> T list -> T * T list
    3.10 -  val ~$$ : Symbol.symbol -> T list -> T * T list
    3.11 -  val $$$ : Symbol.symbol -> T list -> T list * T list
    3.12 -  val ~$$$ : Symbol.symbol -> T list -> T list * T list
    3.13    val content: T list -> string
    3.14    val range: T list -> Position.range
    3.15    val split_lines: T list -> T list list
    3.16 @@ -19,24 +16,28 @@
    3.17    val trim_lines: T list -> T list
    3.18    val is_eof: T -> bool
    3.19    val stopper: T Scan.stopper
    3.20 -  val !!! : Scan.message -> (T list -> 'a) -> T list -> 'a
    3.21 -  val scan_pos: T list -> Position.T * T list
    3.22 -  val scan_string_q: string -> T list -> (Position.T * (T list * Position.T)) * T list
    3.23 -  val scan_string_qq: string -> T list -> (Position.T * (T list * Position.T)) * T list
    3.24 -  val scan_string_bq: string -> T list -> (Position.T * (T list * Position.T)) * T list
    3.25 -  val recover_string_q: T list -> T list * T list
    3.26 -  val recover_string_qq: T list -> T list * T list
    3.27 -  val recover_string_bq: T list -> T list * T list
    3.28 +  val !!! : Scan.message -> 'a scanner -> 'a scanner
    3.29 +  val $$ : Symbol.symbol -> T scanner
    3.30 +  val ~$$ : Symbol.symbol -> T scanner
    3.31 +  val $$$ : Symbol.symbol -> T list scanner
    3.32 +  val ~$$$ : Symbol.symbol -> T list scanner
    3.33 +  val scan_pos: Position.T scanner
    3.34 +  val scan_string_q: string -> (Position.T * (T list * Position.T)) scanner
    3.35 +  val scan_string_qq: string -> (Position.T * (T list * Position.T)) scanner
    3.36 +  val scan_string_bq: string -> (Position.T * (T list * Position.T)) scanner
    3.37 +  val recover_string_q: T list scanner
    3.38 +  val recover_string_qq: T list scanner
    3.39 +  val recover_string_bq: T list scanner
    3.40    val quote_string_q: string -> string
    3.41    val quote_string_qq: string -> string
    3.42    val quote_string_bq: string -> string
    3.43    val cartouche_content: T list -> T list
    3.44 -  val scan_cartouche: string -> T list -> T list * T list
    3.45 -  val scan_cartouche_content: string -> T list -> T list * T list
    3.46 -  val recover_cartouche: T list -> T list * T list
    3.47 -  val scan_comment: string -> T list -> T list * T list
    3.48 -  val scan_comment_body: string -> T list -> T list * T list
    3.49 -  val recover_comment: T list -> T list * T list
    3.50 +  val scan_cartouche: string -> T list scanner
    3.51 +  val scan_cartouche_content: string -> T list scanner
    3.52 +  val recover_cartouche: T list scanner
    3.53 +  val scan_comment: string -> T list scanner
    3.54 +  val scan_comment_body: string -> T list scanner
    3.55 +  val recover_comment: T list scanner
    3.56    val source: Position.T -> (Symbol.symbol, 'a) Source.source ->
    3.57      (T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source
    3.58    type text = string
    3.59 @@ -44,10 +45,10 @@
    3.60    val implode_range: Position.range -> T list -> text * Position.range
    3.61    val explode: text * Position.T -> T list
    3.62    val explode0: string -> T list
    3.63 -  val scan_ident: T list -> T list * T list
    3.64 +  val scan_ident: T list scanner
    3.65    val is_identifier: string -> bool
    3.66 -  val scan_nat: T list -> T list * T list
    3.67 -  val scan_float: T list -> T list * T list
    3.68 +  val scan_nat: T list scanner
    3.69 +  val scan_float: T list scanner
    3.70  end;
    3.71  
    3.72  structure Symbol_Pos: SYMBOL_POS =
    3.73 @@ -56,6 +57,7 @@
    3.74  (* type T *)
    3.75  
    3.76  type T = Symbol.symbol * Position.T;
    3.77 +type 'a scanner = T list -> 'a * T list;
    3.78  
    3.79  fun symbol ((s, _): T) = s;
    3.80  
    3.81 @@ -97,7 +99,7 @@
    3.82  
    3.83  (* basic scanners *)
    3.84  
    3.85 -fun !!! text scan =
    3.86 +fun !!! text (scan: 'a scanner) =
    3.87    let
    3.88      fun get_pos [] = " (end-of-input)"
    3.89        | get_pos ((_, pos) :: _) = Position.here pos;
    3.90 @@ -317,3 +319,5 @@
    3.91    val $$$ = Symbol_Pos.$$$;
    3.92    val ~$$$ = Symbol_Pos.~$$$;
    3.93  end;
    3.94 +
    3.95 +type 'a scanner = 'a Symbol_Pos.scanner;
     4.1 --- a/src/Pure/Syntax/lexicon.ML	Sun Jan 14 14:11:02 2018 +0100
     4.2 +++ b/src/Pure/Syntax/lexicon.ML	Sun Jan 14 15:06:27 2018 +0100
     4.3 @@ -12,13 +12,13 @@
     4.4      val free: string -> term
     4.5      val var: indexname -> term
     4.6    end
     4.7 -  val scan_id: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
     4.8 -  val scan_longid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
     4.9 -  val scan_tid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
    4.10 -  val scan_hex: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
    4.11 -  val scan_bin: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
    4.12 -  val scan_var: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
    4.13 -  val scan_tvar: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
    4.14 +  val scan_id: Symbol_Pos.T list scanner
    4.15 +  val scan_longid: Symbol_Pos.T list scanner
    4.16 +  val scan_tid: Symbol_Pos.T list scanner
    4.17 +  val scan_hex: Symbol_Pos.T list scanner
    4.18 +  val scan_bin: Symbol_Pos.T list scanner
    4.19 +  val scan_var: Symbol_Pos.T list scanner
    4.20 +  val scan_tvar: Symbol_Pos.T list scanner
    4.21    val is_tid: string -> bool
    4.22    datatype token_kind =
    4.23      Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy | FloatSy |