Symbol.stopper;
authorwenzelm
Mon May 18 17:57:47 1998 +0200 (1998-05-18)
changeset 4938c8bbbf3c59fa
parent 4937 e3132cf1d68e
child 4939 33af5d3dae1f
Symbol.stopper;
src/Pure/Syntax/lexicon.ML
src/Pure/Syntax/symbol.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Thy/thy_scan.ML
src/Pure/section_utils.ML
     1.1 --- a/src/Pure/Syntax/lexicon.ML	Mon May 18 17:57:16 1998 +0200
     1.2 +++ b/src/Pure/Syntax/lexicon.ML	Mon May 18 17:57:47 1998 +0200
     1.3 @@ -236,7 +236,7 @@
     1.4  fun implode_xstr cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs));
     1.5  
     1.6  fun explode_xstr str =
     1.7 -  #1 (Scan.error (Scan.finite Symbol.eof scan_str) (Symbol.explode str));
     1.8 +  #1 (Scan.error (Scan.finite Symbol.stopper scan_str) (Symbol.explode str));
     1.9  
    1.10  
    1.11  
    1.12 @@ -263,7 +263,7 @@
    1.13        scan_str >> (Some o StrSy o implode_xstr) ||
    1.14        Scan.one Symbol.is_blank >> K None;
    1.15    in
    1.16 -    (case Scan.error (Scan.finite Symbol.eof (Scan.repeat scan_token)) chs of
    1.17 +    (case Scan.error (Scan.finite Symbol.stopper (Scan.repeat scan_token)) chs of
    1.18        (toks, []) => mapfilter I toks @ [EndToken]
    1.19      | (_, cs) => error ("Inner lexical error at: " ^ quote (implode cs)))
    1.20    end;
    1.21 @@ -297,7 +297,7 @@
    1.22  (* indexname *)
    1.23  
    1.24  fun indexname cs =
    1.25 -  (case Scan.error (Scan.finite Symbol.eof (Scan.option scan_vname)) cs of
    1.26 +  (case Scan.error (Scan.finite Symbol.stopper (Scan.option scan_vname)) cs of
    1.27      (Some xi, []) => xi
    1.28    | _ => error ("Lexical error in variable name: " ^ quote (implode cs)));
    1.29  
    1.30 @@ -317,7 +317,7 @@
    1.31        $$ "?" |-- scan_vname >> var ||
    1.32        Scan.any Symbol.not_eof >> (free o implode);
    1.33    in
    1.34 -    #1 (Scan.error (Scan.finite Symbol.eof scan) (Symbol.explode str))
    1.35 +    #1 (Scan.error (Scan.finite Symbol.stopper scan) (Symbol.explode str))
    1.36    end;
    1.37  
    1.38  
     2.1 --- a/src/Pure/Syntax/symbol.ML	Mon May 18 17:57:16 1998 +0200
     2.2 +++ b/src/Pure/Syntax/symbol.ML	Mon May 18 17:57:47 1998 +0200
     2.3 @@ -12,6 +12,7 @@
     2.4    val eof: symbol
     2.5    val is_eof: symbol -> bool
     2.6    val not_eof: symbol -> bool
     2.7 +  val stopper: symbol * (symbol -> bool)
     2.8    val is_ascii: symbol -> bool
     2.9    val is_letter: symbol -> bool
    2.10    val is_digit: symbol -> bool
    2.11 @@ -170,6 +171,7 @@
    2.12  
    2.13  fun is_eof s = s = eof;
    2.14  fun not_eof s = s <> eof;
    2.15 +val stopper = (eof, is_eof);
    2.16  
    2.17  fun is_ascii s = size s = 1 andalso ord s < 128;
    2.18  
    2.19 @@ -217,7 +219,7 @@
    2.20  fun sym_explode str =
    2.21    let val chs = explode str in
    2.22      if no_syms chs then chs     (*tune trivial case*)
    2.23 -    else map symbol (#1 (Scan.error (Scan.finite eof (Scan.repeat scan)) chs))
    2.24 +    else map symbol (#1 (Scan.error (Scan.finite stopper (Scan.repeat scan)) chs))
    2.25    end;
    2.26  
    2.27  
     3.1 --- a/src/Pure/Syntax/syn_ext.ML	Mon May 18 17:57:16 1998 +0200
     3.2 +++ b/src/Pure/Syntax/syn_ext.ML	Mon May 18 17:57:47 1998 +0200
     3.3 @@ -189,7 +189,7 @@
     3.4      $$ "'" -- Scan.one Symbol.is_blank >> K None;
     3.5  
     3.6    val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (Scan.one (not_equal "'"));
     3.7 -  val read_symbs = mapfilter I o #1 o Scan.error (Scan.finite Symbol.eof scan_symbs);
     3.8 +  val read_symbs = mapfilter I o #1 o Scan.error (Scan.finite Symbol.stopper scan_symbs);
     3.9  in
    3.10    val read_mixfix = read_symbs o Symbol.explode;
    3.11  end;
     4.1 --- a/src/Pure/Thy/thy_scan.ML	Mon May 18 17:57:16 1998 +0200
     4.2 +++ b/src/Pure/Thy/thy_scan.ML	Mon May 18 17:57:47 1998 +0200
     4.3 @@ -144,7 +144,7 @@
     4.4      val scan_toks = Scan.repeat (scan_token lex);
     4.5      val ignore = fn (Ignore, _, _) => true | _ => false;
     4.6    in
     4.7 -    (case Scan.error (Scan.finite' Symbol.eof scan_toks) (Some 1, chs) of
     4.8 +    (case Scan.error (Scan.finite' Symbol.stopper scan_toks) (Some 1, chs) of
     4.9        (toks, (n, [])) => filter_out ignore toks @ [token EOF n "end-of-file"]
    4.10      | (_, (n, cs)) => error (lex_err n ("Bad input " ^ quote (beginning cs))))
    4.11    end;
     5.1 --- a/src/Pure/section_utils.ML	Mon May 18 17:57:16 1998 +0200
     5.2 +++ b/src/Pure/section_utils.ML	Mon May 18 17:57:47 1998 +0200
     5.3 @@ -34,7 +34,7 @@
     5.4  (*Skipping initial blanks, find the first identifier*)	(* FIXME *)
     5.5  fun scan_to_id s = 
     5.6      s |> Symbol.explode
     5.7 -    |> Scan.error (Scan.finite Symbol.eof
     5.8 +    |> Scan.error (Scan.finite Symbol.stopper
     5.9        (!! (fn _ => "Expected to find an identifier in " ^ s)
    5.10          (Scan.any Symbol.is_blank |-- Syntax.scan_id)))
    5.11      |> #1;