moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
authorwenzelm
Thu Mar 19 15:22:53 2009 +0100 (2009-03-19)
changeset 305869674f64a0702
parent 30585 6b2ba4666336
child 30587 ad19c99529eb
moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
scan_comment: recovered change_prompt;
moved read_antiq to outer_lex.ML;
src/Pure/General/symbol_pos.ML
src/Pure/Isar/outer_lex.ML
     1.1 --- a/src/Pure/General/symbol_pos.ML	Thu Mar 19 13:28:55 2009 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Thu Mar 19 15:22:53 2009 +0100
     1.3 @@ -20,7 +20,11 @@
     1.4    val is_eof: T -> bool
     1.5    val stopper: T Scan.stopper
     1.6    val !!! : string -> (T list -> 'a) -> T list -> 'a
     1.7 +  val change_prompt: ('a -> 'b) -> 'a -> 'b
     1.8    val scan_pos: T list -> Position.T * T list
     1.9 +  val scan_string: T list -> (Position.T * (T list * Position.T)) * T list
    1.10 +  val scan_alt_string: T list -> (Position.T * (T list * Position.T)) * T list
    1.11 +  val scan_quoted: T list -> T list * T list
    1.12    val scan_comment: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
    1.13      T list -> T list * T list
    1.14    val scan_comment_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
    1.15 @@ -83,12 +87,44 @@
    1.16        (case msg of NONE => "" | SOME s => "\n" ^ s);
    1.17    in Scan.!! err scan end;
    1.18  
    1.19 +fun change_prompt scan = Scan.prompt "# " scan;
    1.20 +
    1.21  fun $$$ s = Scan.one (fn x => symbol x = s) >> single;
    1.22  fun ~$$$ s = Scan.one (fn x => symbol x <> s) >> single;
    1.23  
    1.24  val scan_pos = Scan.ahead (Scan.one (K true)) >> (fn (_, pos): T => pos);
    1.25  
    1.26  
    1.27 +(* Isabelle strings *)
    1.28 +
    1.29 +local
    1.30 +
    1.31 +val char_code =
    1.32 +  Scan.one (Symbol.is_ascii_digit o symbol) --
    1.33 +  Scan.one (Symbol.is_ascii_digit o symbol) --
    1.34 +  Scan.one (Symbol.is_ascii_digit o symbol) :|--
    1.35 +  (fn (((a, pos), (b, _)), (c, _)) =>
    1.36 +    let val (n, _) = Library.read_int [a, b, c]
    1.37 +    in if n <= 255 then Scan.succeed [(chr n, pos)] else Scan.fail end);
    1.38 +
    1.39 +fun scan_str q =
    1.40 +  $$$ "\\" |-- !!! "bad escape character in string" ($$$ q || $$$ "\\" || char_code) ||
    1.41 +  Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single;
    1.42 +
    1.43 +fun scan_strs q =
    1.44 +  (scan_pos --| $$$ q) -- !!! "missing quote at end of string"
    1.45 +    (change_prompt ((Scan.repeat (scan_str q) >> flat) -- ($$$ q |-- scan_pos)));
    1.46 +
    1.47 +in
    1.48 +
    1.49 +val scan_string = scan_strs "\"";
    1.50 +val scan_alt_string = scan_strs "`";
    1.51 +
    1.52 +val scan_quoted = Scan.trace (scan_string || scan_alt_string) >> #2;
    1.53 +
    1.54 +end;
    1.55 +
    1.56 +
    1.57  (* ML-style comments *)
    1.58  
    1.59  local
    1.60 @@ -99,7 +135,7 @@
    1.61    Scan.lift ($$$ "*" --| Scan.ahead (~$$$ ")")) ||
    1.62    Scan.lift (Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s)) >> single;
    1.63  
    1.64 -val scan_body = Scan.pass 0 (Scan.repeat scan_cmt >> flat);
    1.65 +val scan_body = change_prompt (Scan.pass 0 (Scan.repeat scan_cmt >> flat));
    1.66  
    1.67  in
    1.68  
     2.1 --- a/src/Pure/Isar/outer_lex.ML	Thu Mar 19 13:28:55 2009 +0100
     2.2 +++ b/src/Pure/Isar/outer_lex.ML	Thu Mar 19 15:22:53 2009 +0100
     2.3 @@ -51,13 +51,14 @@
     2.4    val closure: token -> token
     2.5    val ident_or_symbolic: string -> bool
     2.6    val !!! : string -> (Symbol_Pos.T list -> 'a) -> Symbol_Pos.T list -> 'a
     2.7 -  val scan_quoted: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
     2.8    val source_proper: (token, 'a) Source.source -> (token, (token, 'a) Source.source) Source.source
     2.9    val source': {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
    2.10      (Symbol_Pos.T, 'a) Source.source -> (token, (Symbol_Pos.T, 'a) Source.source) Source.source
    2.11    val source: {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
    2.12      Position.T -> (Symbol.symbol, 'a) Source.source -> (token,
    2.13        (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
    2.14 +  val read_antiq: Scan.lexicon -> (token list -> 'a * token list) ->
    2.15 +    Symbol_Pos.T list * Position.T -> 'a
    2.16  end;
    2.17  
    2.18  structure OuterLex: OUTER_LEX =
    2.19 @@ -263,8 +264,6 @@
    2.20  
    2.21  fun !!! msg = Symbol_Pos.!!! ("Outer lexical error: " ^ msg);
    2.22  
    2.23 -fun change_prompt scan = Scan.prompt "# " scan;
    2.24 -
    2.25  
    2.26  (* scan symbolic idents *)
    2.27  
    2.28 @@ -286,36 +285,6 @@
    2.29    | ident_or_symbolic s = Syntax.is_identifier s orelse is_symid s;
    2.30  
    2.31  
    2.32 -(* scan strings *)
    2.33 -
    2.34 -local
    2.35 -
    2.36 -val char_code =
    2.37 -  Scan.one (Symbol.is_ascii_digit o symbol) --
    2.38 -  Scan.one (Symbol.is_ascii_digit o symbol) --
    2.39 -  Scan.one (Symbol.is_ascii_digit o symbol) :|--
    2.40 -  (fn (((a, pos), (b, _)), (c, _)) =>
    2.41 -    let val (n, _) = Library.read_int [a, b, c]
    2.42 -    in if n <= 255 then Scan.succeed [(chr n, pos)] else Scan.fail end);
    2.43 -
    2.44 -fun scan_str q =
    2.45 -  $$$ "\\" |-- !!! "bad escape character in string" ($$$ q || $$$ "\\" || char_code) ||
    2.46 -  Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single;
    2.47 -
    2.48 -fun scan_strs q =
    2.49 -  (Symbol_Pos.scan_pos --| $$$ q) -- !!! "missing quote at end of string"
    2.50 -    (change_prompt ((Scan.repeat (scan_str q) >> flat) -- ($$$ q |-- Symbol_Pos.scan_pos)));
    2.51 -
    2.52 -in
    2.53 -
    2.54 -val scan_string = scan_strs "\"";
    2.55 -val scan_alt_string = scan_strs "`";
    2.56 -
    2.57 -val scan_quoted = Scan.trace (scan_string || scan_alt_string) >> #2;
    2.58 -
    2.59 -end;
    2.60 -
    2.61 -
    2.62  (* scan verbatim text *)
    2.63  
    2.64  val scan_verb =
    2.65 @@ -324,7 +293,8 @@
    2.66  
    2.67  val scan_verbatim =
    2.68    (Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") -- !!! "missing end of verbatim text"
    2.69 -    (change_prompt ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
    2.70 +    (Symbol_Pos.change_prompt
    2.71 +      ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
    2.72  
    2.73  
    2.74  (* scan space *)
    2.75 @@ -346,7 +316,7 @@
    2.76  
    2.77  val scan_malformed =
    2.78    $$$ Symbol.malformed |--
    2.79 -    change_prompt (Scan.many (Symbol.is_regular o symbol))
    2.80 +    Symbol_Pos.change_prompt (Scan.many (Symbol.is_regular o symbol))
    2.81    --| Scan.option ($$$ Symbol.end_malformed);
    2.82  
    2.83  
    2.84 @@ -366,8 +336,8 @@
    2.85    Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.untabify_content ss), Slot);
    2.86  
    2.87  fun scan (lex1, lex2) = !!! "bad input"
    2.88 -  (scan_string >> token_range String ||
    2.89 -    scan_alt_string >> token_range AltString ||
    2.90 +  (Symbol_Pos.scan_string >> token_range String ||
    2.91 +    Symbol_Pos.scan_alt_string >> token_range AltString ||
    2.92      scan_verbatim >> token_range Verbatim ||
    2.93      scan_comment >> token_range Comment ||
    2.94      scan_space >> token Space ||
    2.95 @@ -401,4 +371,20 @@
    2.96  
    2.97  end;
    2.98  
    2.99 +
   2.100 +(* read_antiq *)
   2.101 +
   2.102 +fun read_antiq lex scan (syms, pos) =
   2.103 +  let
   2.104 +    fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^
   2.105 +      "@{" ^ Symbol_Pos.content syms ^ "}");
   2.106 +
   2.107 +    val res =
   2.108 +      Source.of_list syms
   2.109 +      |> source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
   2.110 +      |> source_proper
   2.111 +      |> Source.source stopper (Scan.error (Scan.bulk scan)) NONE
   2.112 +      |> Source.exhaust;
   2.113 +  in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
   2.114 +
   2.115  end;