tuned -- more direct err_prefix;
authorwenzelm
Mon Jan 20 20:04:52 2014 +0100 (2014-01-20)
changeset 5510575815b3b38a1
parent 55104 8284c0d5bf52
child 55106 080c0006e917
tuned -- more direct err_prefix;
src/Pure/General/antiquote.ML
src/Pure/General/symbol_pos.ML
src/Pure/Isar/token.ML
src/Pure/ML/ml_lex.ML
src/Pure/Syntax/lexicon.ML
     1.1 --- a/src/Pure/General/antiquote.ML	Mon Jan 20 19:47:31 2014 +0100
     1.2 +++ b/src/Pure/General/antiquote.ML	Mon Jan 20 20:04:52 2014 +0100
     1.3 @@ -50,7 +50,7 @@
     1.4  
     1.5  val scan_ant =
     1.6    Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
     1.7 -  Scan.trace (Symbol_Pos.scan_cartouche (fn s => Symbol_Pos.!!! (fn () => err_prefix ^ s))) >> #2 ||
     1.8 +  Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >> #2 ||
     1.9    Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
    1.10  
    1.11  in
     2.1 --- a/src/Pure/General/symbol_pos.ML	Mon Jan 20 19:47:31 2014 +0100
     2.2 +++ b/src/Pure/General/symbol_pos.ML	Mon Jan 20 20:04:52 2014 +0100
     2.3 @@ -27,14 +27,11 @@
     2.4    val quote_string_q: string -> string
     2.5    val quote_string_qq: string -> string
     2.6    val quote_string_bq: string -> string
     2.7 -  val scan_cartouche: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
     2.8 -    T list -> T list * T list
     2.9 +  val scan_cartouche: string -> T list -> T list * T list
    2.10    val recover_cartouche: T list -> T list * T list
    2.11    val cartouche_content: T list -> T list
    2.12 -  val scan_comment: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
    2.13 -    T list -> T list * T list
    2.14 -  val scan_comment_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
    2.15 -    T list -> T list * T list
    2.16 +  val scan_comment: string -> T list -> T list * T list
    2.17 +  val scan_comment_body: string -> T list -> T list * T list
    2.18    val recover_comment: T list -> T list * T list
    2.19    val source: Position.T -> (Symbol.symbol, 'a) Source.source ->
    2.20      (T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source
    2.21 @@ -168,9 +165,9 @@
    2.22          $$ "\\<close>" >> pair (d - 1)
    2.23        else Scan.fail)));
    2.24  
    2.25 -fun scan_cartouche cut =
    2.26 +fun scan_cartouche err_prefix =
    2.27    Scan.ahead ($$ "\\<open>") |--
    2.28 -    cut "unclosed text cartouche"
    2.29 +    !!! (fn () => err_prefix ^ "unclosed text cartouche")
    2.30        (change_prompt (Scan.provide (fn d => d = 0) 0 scan_cartouche_depth));
    2.31  
    2.32  val recover_cartouche = Scan.pass 0 scan_cartouche_depth;
    2.33 @@ -206,11 +203,13 @@
    2.34  
    2.35  in
    2.36  
    2.37 -fun scan_comment cut =
    2.38 -  $$$ "(" @@@ $$$ "*" @@@ cut "missing end of comment" (scan_body @@@ $$$ "*" @@@ $$$ ")");
    2.39 +fun scan_comment err_prefix =
    2.40 +  $$$ "(" @@@ $$$ "*" @@@
    2.41 +    !!! (fn () => err_prefix ^ "missing end of comment") (scan_body @@@ $$$ "*" @@@ $$$ ")");
    2.42  
    2.43 -fun scan_comment_body cut =
    2.44 -  $$$ "(" |-- $$$ "*" |-- cut "missing end of comment" (scan_body --| $$$ "*" --| $$$ ")");
    2.45 +fun scan_comment_body err_prefix =
    2.46 +  $$$ "(" |-- $$$ "*" |--
    2.47 +    !!! (fn () => err_prefix ^ "missing end of comment") (scan_body --| $$$ "*" --| $$$ ")");
    2.48  
    2.49  val recover_comment =
    2.50    $$$ "(" @@@ $$$ "*" @@@ scan_cmts;
     3.1 --- a/src/Pure/Isar/token.ML	Mon Jan 20 19:47:31 2014 +0100
     3.2 +++ b/src/Pure/Isar/token.ML	Mon Jan 20 20:04:52 2014 +0100
     3.3 @@ -337,7 +337,7 @@
     3.4  
     3.5  val scan_cartouche =
     3.6    Symbol_Pos.scan_pos --
     3.7 -    ((Symbol_Pos.scan_cartouche !!! >> Symbol_Pos.cartouche_content) -- Symbol_Pos.scan_pos);
     3.8 +    ((Symbol_Pos.scan_cartouche err_prefix >> Symbol_Pos.cartouche_content) -- Symbol_Pos.scan_pos);
     3.9  
    3.10  
    3.11  (* scan space *)
    3.12 @@ -352,7 +352,7 @@
    3.13  (* scan comment *)
    3.14  
    3.15  val scan_comment =
    3.16 -  Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body !!! -- Symbol_Pos.scan_pos);
    3.17 +  Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body err_prefix -- Symbol_Pos.scan_pos);
    3.18  
    3.19  
    3.20  
     4.1 --- a/src/Pure/ML/ml_lex.ML	Mon Jan 20 19:47:31 2014 +0100
     4.2 +++ b/src/Pure/ML/ml_lex.ML	Mon Jan 20 20:04:52 2014 +0100
     4.3 @@ -137,7 +137,9 @@
     4.4  
     4.5  open Basic_Symbol_Pos;
     4.6  
     4.7 -fun !!! msg = Symbol_Pos.!!! (fn () => "SML lexical error: " ^ msg);
     4.8 +val err_prefix = "SML lexical error: ";
     4.9 +
    4.10 +fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg);
    4.11  
    4.12  
    4.13  (* blanks *)
    4.14 @@ -261,7 +263,7 @@
    4.15   (scan_char >> token Char ||
    4.16    scan_string >> token String ||
    4.17    scan_blanks1 >> token Space ||
    4.18 -  Symbol_Pos.scan_comment !!! >> token Comment ||
    4.19 +  Symbol_Pos.scan_comment err_prefix >> token Comment ||
    4.20    Scan.max token_leq
    4.21     (scan_keyword >> token Keyword)
    4.22     (scan_word >> token Word ||
     5.1 --- a/src/Pure/Syntax/lexicon.ML	Mon Jan 20 19:47:31 2014 +0100
     5.2 +++ b/src/Pure/Syntax/lexicon.ML	Mon Jan 20 20:04:52 2014 +0100
     5.3 @@ -87,7 +87,9 @@
     5.4  
     5.5  open Basic_Symbol_Pos;
     5.6  
     5.7 -fun !!! msg = Symbol_Pos.!!! (fn () => "Inner lexical error: " ^ msg);
     5.8 +val err_prefix = "Inner lexical error: ";
     5.9 +
    5.10 +fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg);
    5.11  
    5.12  val scan_id = Symbol_Pos.scan_ident;
    5.13  val scan_longid = scan_id @@@ (Scan.repeat1 ($$$ "." @@@ scan_id) >> flat);
    5.14 @@ -258,8 +260,8 @@
    5.15      val scan_lit = Scan.literal lex >> token Literal;
    5.16  
    5.17      val scan_token =
    5.18 -      Symbol_Pos.scan_cartouche !!! >> token Cartouche ||
    5.19 -      Symbol_Pos.scan_comment !!! >> token Comment ||
    5.20 +      Symbol_Pos.scan_cartouche err_prefix >> token Cartouche ||
    5.21 +      Symbol_Pos.scan_comment err_prefix >> token Comment ||
    5.22        Scan.max token_leq scan_lit scan_val ||
    5.23        scan_str >> token StrSy ||
    5.24        Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol) >> token Space;