tuned signature;
authorwenzelm
Tue Mar 29 20:53:52 2016 +0200 (2016-03-29)
changeset 6275124e2b098bf44
parent 62750 3f8f7aa1b11e
child 62752 d09d71223e7a
tuned signature;
src/Pure/General/symbol_pos.ML
src/Pure/Syntax/lexicon.ML
src/Pure/Syntax/simple_syntax.ML
     1.1 --- a/src/Pure/General/symbol_pos.ML	Tue Mar 29 20:52:19 2016 +0200
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Tue Mar 29 20:53:52 2016 +0200
     1.3 @@ -42,6 +42,7 @@
     1.4    val implode: T list -> text
     1.5    val implode_range: Position.range -> T list -> text * Position.range
     1.6    val explode: text * Position.T -> T list
     1.7 +  val explode0: string -> T list
     1.8    val scan_ident: T list -> T list * T list
     1.9    val is_identifier: string -> bool
    1.10  end;
    1.11 @@ -271,6 +272,8 @@
    1.12          (Symbol.explode str) ([], Position.reset_range pos);
    1.13    in fold (fn (s, p) => if s = Symbol.DEL then I else cons (s, p)) res [] end;
    1.14  
    1.15 +fun explode0 str = explode (str, Position.none);
    1.16 +
    1.17  
    1.18  (* identifiers *)
    1.19  
    1.20 @@ -289,7 +292,7 @@
    1.21  
    1.22  fun is_identifier s =
    1.23    Symbol.is_ascii_identifier s orelse
    1.24 -    (case try (Scan.finite stopper scan_ident) (explode (s, Position.none)) of
    1.25 +    (case try (Scan.finite stopper scan_ident) (explode0 s) of
    1.26        SOME (_, []) => true
    1.27      | _ => false);
    1.28  
    1.29 @@ -302,4 +305,3 @@
    1.30    val $$$ = Symbol_Pos.$$$;
    1.31    val ~$$$ = Symbol_Pos.~$$$;
    1.32  end;
    1.33 -
     2.1 --- a/src/Pure/Syntax/lexicon.ML	Tue Mar 29 20:52:19 2016 +0200
     2.2 +++ b/src/Pure/Syntax/lexicon.ML	Tue Mar 29 20:53:52 2016 +0200
     2.3 @@ -327,7 +327,7 @@
     2.4  (* indexname *)
     2.5  
     2.6  fun read_indexname s =
     2.7 -  (case Scan.read Symbol_Pos.stopper scan_indexname (Symbol_Pos.explode (s, Position.none)) of
     2.8 +  (case Scan.read Symbol_Pos.stopper scan_indexname (Symbol_Pos.explode0 s) of
     2.9      SOME xi => xi
    2.10    | _ => error ("Lexical error in variable name: " ^ quote s));
    2.11  
    2.12 @@ -341,14 +341,14 @@
    2.13          >> Syntax.var ||
    2.14        Scan.many (Symbol.not_eof o Symbol_Pos.symbol)
    2.15          >> (Syntax.free o implode o map Symbol_Pos.symbol);
    2.16 -  in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none))) end;
    2.17 +  in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode0 str)) end;
    2.18  
    2.19  
    2.20  (* read_variable *)
    2.21  
    2.22  fun read_variable str =
    2.23    let val scan = $$ "?" |-- scan_indexname || scan_indexname
    2.24 -  in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none)) end;
    2.25 +  in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode0 str) end;
    2.26  
    2.27  
    2.28  (* read numbers *)
    2.29 @@ -361,10 +361,10 @@
    2.30  
    2.31  in
    2.32  
    2.33 -fun read_nat s = nat (Symbol_Pos.explode (s, Position.none));
    2.34 +fun read_nat s = nat (Symbol_Pos.explode0 s);
    2.35  
    2.36  fun read_int s =
    2.37 -  (case Symbol_Pos.explode (s, Position.none) of
    2.38 +  (case Symbol_Pos.explode0 s of
    2.39      ("-", _) :: cs => Option.map ~ (nat cs)
    2.40    | cs => nat cs);
    2.41  
     3.1 --- a/src/Pure/Syntax/simple_syntax.ML	Tue Mar 29 20:52:19 2016 +0200
     3.2 +++ b/src/Pure/Syntax/simple_syntax.ML	Tue Mar 29 20:53:52 2016 +0200
     3.3 @@ -21,7 +21,7 @@
     3.4  
     3.5  fun read scan s =
     3.6    (case
     3.7 -      Symbol_Pos.explode (s, Position.none) |>
     3.8 +      Symbol_Pos.explode0 s |>
     3.9        Lexicon.tokenize lexicon false |>
    3.10        filter Lexicon.is_proper |>
    3.11        Scan.read Lexicon.stopper scan of