tuned signature;
authorwenzelm
Mon Jan 20 20:38:51 2014 +0100 (2014-01-20)
changeset 551071a29ea173bf9
parent 55106 080c0006e917
child 55108 0b7a0c1fdf7e
tuned signature;
src/Pure/General/antiquote.ML
src/Pure/General/symbol_pos.ML
src/Pure/Isar/token.ML
src/Pure/Syntax/lexicon.ML
     1.1 --- a/src/Pure/General/antiquote.ML	Mon Jan 20 20:24:44 2014 +0100
     1.2 +++ b/src/Pure/General/antiquote.ML	Mon Jan 20 20:38:51 2014 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4  val err_prefix = "Antiquotation lexical error: ";
     1.5  
     1.6  val scan_txt =
     1.7 -  $$$ "@" --| Scan.ahead (~$$$ "{") ||
     1.8 +  $$$ "@" --| Scan.ahead (~$$ "{") ||
     1.9    Scan.one (fn (s, _) => s <> "@" andalso Symbol.is_regular s) >> single;
    1.10  
    1.11  val scan_ant =
    1.12 @@ -56,9 +56,9 @@
    1.13  in
    1.14  
    1.15  val scan_antiq =
    1.16 -  Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
    1.17 +  Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |--
    1.18      Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace")
    1.19 -      (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
    1.20 +      (Scan.repeat scan_ant -- ($$ "}" |-- Symbol_Pos.scan_pos)))
    1.21    >> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2));
    1.22  
    1.23  val scan_text = scan_antiq >> Antiq || Scan.repeat1 scan_txt >> (Text o flat);
     2.1 --- a/src/Pure/General/symbol_pos.ML	Mon Jan 20 20:24:44 2014 +0100
     2.2 +++ b/src/Pure/General/symbol_pos.ML	Mon Jan 20 20:38:51 2014 +0100
     2.3 @@ -9,6 +9,7 @@
     2.4    type T = Symbol.symbol * Position.T
     2.5    val symbol: T -> Symbol.symbol
     2.6    val $$ : Symbol.symbol -> T list -> T * T list
     2.7 +  val ~$$ : Symbol.symbol -> T list -> T * T list
     2.8    val $$$ : Symbol.symbol -> T list -> T list * T list
     2.9    val ~$$$ : Symbol.symbol -> T list -> T list * T list
    2.10    val content: T list -> string
    2.11 @@ -87,6 +88,8 @@
    2.12  fun change_prompt scan = Scan.prompt "# " scan;
    2.13  
    2.14  fun $$ s = Scan.one (fn x => symbol x = s);
    2.15 +fun ~$$ s = Scan.one (fn x => symbol x <> s);
    2.16 +
    2.17  fun $$$ s = Scan.one (fn x => symbol x = s) >> single;
    2.18  fun ~$$$ s = Scan.one (fn x => symbol x <> s) >> single;
    2.19  
    2.20 @@ -278,6 +281,7 @@
    2.21  structure Basic_Symbol_Pos =   (*not open by default*)
    2.22  struct
    2.23    val $$ = Symbol_Pos.$$;
    2.24 +  val ~$$ = Symbol_Pos.~$$;
    2.25    val $$$ = Symbol_Pos.$$$;
    2.26    val ~$$$ = Symbol_Pos.~$$$;
    2.27  end;
     3.1 --- a/src/Pure/Isar/token.ML	Mon Jan 20 20:24:44 2014 +0100
     3.2 +++ b/src/Pure/Isar/token.ML	Mon Jan 20 20:38:51 2014 +0100
     3.3 @@ -321,15 +321,15 @@
     3.4  (* scan verbatim text *)
     3.5  
     3.6  val scan_verb =
     3.7 -  $$$ "*" --| Scan.ahead (~$$$ "}") ||
     3.8 +  $$$ "*" --| Scan.ahead (~$$ "}") ||
     3.9    Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single;
    3.10  
    3.11  val scan_verbatim =
    3.12 -  Scan.ahead ($$$ "{" -- $$$ "*") |--
    3.13 +  Scan.ahead ($$ "{" -- $$ "*") |--
    3.14      !!! "unclosed verbatim text"
    3.15 -      ((Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") --
    3.16 +      ((Symbol_Pos.scan_pos --| $$ "{" --| $$ "*") --
    3.17          Symbol_Pos.change_prompt
    3.18 -          ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
    3.19 +          ((Scan.repeat scan_verb >> flat) -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos)));
    3.20  
    3.21  val recover_verbatim =
    3.22    $$$ "{" @@@ $$$ "*" @@@ (Scan.repeat scan_verb >> flat);
     4.1 --- a/src/Pure/Syntax/lexicon.ML	Mon Jan 20 20:24:44 2014 +0100
     4.2 +++ b/src/Pure/Syntax/lexicon.ML	Mon Jan 20 20:38:51 2014 +0100
     4.3 @@ -210,11 +210,11 @@
     4.4  (* str tokens *)
     4.5  
     4.6  val scan_chr =
     4.7 -  $$$ "\\" |-- $$$ "'" ||
     4.8 +  $$ "\\" |-- $$$ "'" ||
     4.9    Scan.one
    4.10      ((fn s => s <> "\\" andalso s <> "'" andalso Symbol.is_regular s) o
    4.11        Symbol_Pos.symbol) >> single ||
    4.12 -  $$$ "'" --| Scan.ahead (~$$$ "'");
    4.13 +  $$$ "'" --| Scan.ahead (~$$ "'");
    4.14  
    4.15  val scan_str =
    4.16    Scan.ahead ($$ "'" -- $$ "'") |--
    4.17 @@ -222,7 +222,7 @@
    4.18        ($$$ "'" @@@ $$$ "'" @@@ (Scan.repeat scan_chr >> flat) @@@ $$$ "'" @@@ $$$ "'");
    4.19  
    4.20  val scan_str_body =
    4.21 -  Scan.ahead ($$$ "'" |-- $$$ "'") |--
    4.22 +  Scan.ahead ($$ "'" |-- $$ "'") |--
    4.23      !!! "unclosed string literal"
    4.24        ($$ "'" |-- $$ "'" |-- (Scan.repeat scan_chr >> flat) --| $$ "'" --| $$ "'");
    4.25  
    4.26 @@ -297,7 +297,7 @@
    4.27  
    4.28      val scan =
    4.29        (scan_id >> map Symbol_Pos.symbol) --
    4.30 -      Scan.optional ($$$ "." |-- scan_nat >> (nat 0 o map Symbol_Pos.symbol)) ~1;
    4.31 +      Scan.optional ($$ "." |-- scan_nat >> (nat 0 o map Symbol_Pos.symbol)) ~1;
    4.32    in
    4.33      scan >>
    4.34        (fn (cs, ~1) => chop_idx (rev cs) []
    4.35 @@ -306,7 +306,7 @@
    4.36  
    4.37  in
    4.38  
    4.39 -val scan_indexname = $$$ "'" |-- scan_vname >> (fn (x, i) => ("'" ^ x, i)) || scan_vname;
    4.40 +val scan_indexname = $$ "'" |-- scan_vname >> (fn (x, i) => ("'" ^ x, i)) || scan_vname;
    4.41  
    4.42  end;
    4.43  
    4.44 @@ -324,7 +324,7 @@
    4.45  fun read_var str =
    4.46    let
    4.47      val scan =
    4.48 -      $$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof)
    4.49 +      $$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof)
    4.50          >> Syntax.var ||
    4.51        Scan.many (Symbol.is_regular o Symbol_Pos.symbol)
    4.52          >> (Syntax.free o implode o map Symbol_Pos.symbol);
    4.53 @@ -334,7 +334,7 @@
    4.54  (* read_variable *)
    4.55  
    4.56  fun read_variable str =
    4.57 -  let val scan = $$$ "?" |-- scan_indexname || scan_indexname
    4.58 +  let val scan = $$ "?" |-- scan_indexname || scan_indexname
    4.59    in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none)) end;
    4.60  
    4.61