abstract type Scan.stopper;
authorwenzelm
Mon Aug 04 21:24:17 2008 +0200 (2008-08-04)
changeset 277328dbf5761a24a
parent 27731 a7444ded92cf
child 27733 d3d7038fb7b5
abstract type Scan.stopper;
src/Pure/General/source.ML
src/Pure/General/symbol.ML
src/Pure/Isar/args.ML
src/Pure/ML/ml_lex.ML
src/Pure/Syntax/simple_syntax.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/General/source.ML	Mon Aug 04 21:24:15 2008 +0200
     1.2 +++ b/src/Pure/General/source.ML	Mon Aug 04 21:24:17 2008 +0200
     1.3 @@ -21,10 +21,10 @@
     1.4    val of_string: string -> (string, string list) source
     1.5    val exhausted: ('a, 'b) source -> ('a, 'a list) source
     1.6    val tty: (string, unit) source
     1.7 -  val source': 'a -> 'b * ('b -> bool) -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
     1.8 +  val source': 'a -> 'b Scan.stopper -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
     1.9      (bool * (string -> 'a * 'b list -> 'c list * ('a * 'b list))) option ->
    1.10      ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source
    1.11 -  val source: 'a * ('a -> bool) -> ('a list -> 'b list * 'a list) ->
    1.12 +  val source: 'a Scan.stopper -> ('a list -> 'b list * 'a list) ->
    1.13      (bool * (string -> 'a list -> 'b list * 'a list)) option ->
    1.14      ('a, 'd) source -> ('b, ('a, 'd) source) source
    1.15  end;
    1.16 @@ -148,7 +148,7 @@
    1.17          | SOME (interactive, recover) =>
    1.18              (drain (Scan.catch scan) inp handle Fail msg =>
    1.19                (if interactive then Output.error_msg msg else ();
    1.20 -                drain (Scan.unless (Scan.lift (Scan.one (#2 stopper))) (recover msg)) inp)));
    1.21 +                drain (Scan.unless (Scan.lift (Scan.one (Scan.is_stopper stopper))) (recover msg)) inp)));
    1.22    in (ys, (state', unget (xs', src'))) end;
    1.23  
    1.24  fun source' init_state stopper scan recover src =
     2.1 --- a/src/Pure/General/symbol.ML	Mon Aug 04 21:24:15 2008 +0200
     2.2 +++ b/src/Pure/General/symbol.ML	Mon Aug 04 21:24:17 2008 +0200
     2.3 @@ -21,7 +21,7 @@
     2.4    val is_utf8_trailer: symbol -> bool
     2.5    val eof: symbol
     2.6    val is_eof: symbol -> bool
     2.7 -  val stopper: symbol * (symbol -> bool)
     2.8 +  val stopper: symbol Scan.stopper
     2.9    val sync: symbol
    2.10    val is_sync: symbol -> bool
    2.11    val malformed: symbol
    2.12 @@ -120,7 +120,7 @@
    2.13  val eof = "";
    2.14  fun is_eof s = s = eof;
    2.15  fun not_eof s = s <> eof;
    2.16 -val stopper = (eof, is_eof);
    2.17 +val stopper = Scan.stopper (K eof) is_eof;
    2.18  
    2.19  val sync = "\\<^sync>";
    2.20  fun is_sync s = s = sync;
     3.1 --- a/src/Pure/Isar/args.ML	Mon Aug 04 21:24:15 2008 +0200
     3.2 +++ b/src/Pure/Isar/args.ML	Mon Aug 04 21:24:17 2008 +0200
     3.3 @@ -23,7 +23,7 @@
     3.4    val mk_fact: thm list -> T
     3.5    val mk_attribute: (morphism -> attribute) -> T
     3.6    val eof: T
     3.7 -  val stopper: T * (T -> bool)
     3.8 +  val stopper: T Scan.stopper
     3.9    val not_eof: T -> bool
    3.10    type src
    3.11    val src: (string * T list) * Position.T -> src
    3.12 @@ -161,7 +161,7 @@
    3.13  fun is_eof (Arg ((EOF, _, _), _)) = true
    3.14    | is_eof _ = false;
    3.15  
    3.16 -val stopper = (eof, is_eof);
    3.17 +val stopper = Scan.stopper (K eof) is_eof;
    3.18  val not_eof = not o is_eof;
    3.19  
    3.20  
     4.1 --- a/src/Pure/ML/ml_lex.ML	Mon Aug 04 21:24:15 2008 +0200
     4.2 +++ b/src/Pure/ML/ml_lex.ML	Mon Aug 04 21:24:17 2008 +0200
     4.3 @@ -11,7 +11,7 @@
     4.4      Keyword | Ident | LongIdent | TypeVar | Word | Int | Real | Char | String |
     4.5      Space | Comment | Error of string | EOF
     4.6    eqtype token
     4.7 -  val stopper: token * (token -> bool)
     4.8 +  val stopper: token Scan.stopper
     4.9    val is_regular: token -> bool
    4.10    val is_improper: token -> bool
    4.11    val pos_of: token -> string
    4.12 @@ -43,7 +43,7 @@
    4.13  fun is_eof (Token (_, (EOF, _))) = true
    4.14    | is_eof _ = false;
    4.15  
    4.16 -val stopper = (eof, is_eof);
    4.17 +val stopper = Scan.stopper (K eof) is_eof;
    4.18  
    4.19  
    4.20  fun is_regular (Token (_, (Error _, _))) = false
     5.1 --- a/src/Pure/Syntax/simple_syntax.ML	Mon Aug 04 21:24:15 2008 +0200
     5.2 +++ b/src/Pure/Syntax/simple_syntax.ML	Mon Aug 04 21:24:17 2008 +0200
     5.3 @@ -22,7 +22,7 @@
     5.4  val eof = Lexicon.EndToken;
     5.5  fun is_eof tk = tk = Lexicon.EndToken;
     5.6  
     5.7 -val stopper = (eof, is_eof);
     5.8 +val stopper = Scan.stopper (K eof) is_eof;
     5.9  val not_eof = not o is_eof;
    5.10  
    5.11  val lexicon = Scan.make_lexicon
     6.1 --- a/src/Pure/Thy/thy_output.ML	Mon Aug 04 21:24:15 2008 +0200
     6.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Aug 04 21:24:17 2008 +0200
     6.3 @@ -363,12 +363,11 @@
     6.4  
     6.5      (* spans *)
     6.6  
     6.7 -    val stopper =
     6.8 -      ((NONE, (BasicToken (#1 T.stopper), ("", 0))),
     6.9 -        fn (_, (BasicToken x, _)) => #2 T.stopper x | _ => false);
    6.10 +    val is_eof = fn (_, (BasicToken x, _)) => T.is_eof x | _ => false;
    6.11 +    val stopper = Scan.stopper (K (NONE, (BasicToken T.eof, ("", 0)))) is_eof;
    6.12  
    6.13      val cmd = Scan.one (is_some o fst);
    6.14 -    val non_cmd = Scan.one (is_none o fst andf not o #2 stopper) >> #2;
    6.15 +    val non_cmd = Scan.one (is_none o fst andf not o is_eof) >> #2;
    6.16  
    6.17      val comments = Scan.many (comment_token o fst o snd);
    6.18      val blank = Scan.one (blank_token o fst o snd);