tuned signature according to Scala version -- prefer explicit argument;
authorwenzelm
Tue Aug 12 20:18:27 2014 +0200 (2014-08-12)
changeset 57918f5d73caba4e5
parent 57917 8ce97e5d545f
child 57919 a2a7c1de4752
tuned signature according to Scala version -- prefer explicit argument;
src/Doc/antiquote_setup.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Tools/Lifting/lifting_setup.ML
src/HOL/Tools/try0.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/PIDE/document.ML
src/Pure/PIDE/resources.ML
src/Pure/Thy/thy_info.ML
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
src/Tools/Code/code_target.ML
     1.1 --- a/src/Doc/antiquote_setup.ML	Tue Aug 12 18:54:53 2014 +0200
     1.2 +++ b/src/Doc/antiquote_setup.ML	Tue Aug 12 20:18:27 2014 +0200
     1.3 @@ -208,7 +208,7 @@
     1.4    is_some (Keyword.command_keyword name) andalso
     1.5      let
     1.6        val markup =
     1.7 -        Outer_Syntax.scan Position.none name
     1.8 +        Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none name
     1.9          |> maps (Outer_Syntax.command_reports (#2 (Outer_Syntax.get_syntax ())))
    1.10          |> map (snd o fst);
    1.11        val _ = Context_Position.reports ctxt (map (pair pos) markup);
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 12 18:54:53 2014 +0200
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 12 20:18:27 2014 +0200
     2.3 @@ -525,7 +525,7 @@
     2.4      fun do_method named_thms ctxt =
     2.5        let
     2.6          val ref_of_str =
     2.7 -          suffix ";" #> Outer_Syntax.scan Position.none #> Parse_Spec.xthm
     2.8 +          suffix ";" #> Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none #> Parse_Spec.xthm
     2.9            #> fst
    2.10          val thms = named_thms |> maps snd
    2.11          val facts = named_thms |> map (ref_of_str o fst o fst)
    2.12 @@ -551,7 +551,7 @@
    2.13            let
    2.14              val (type_encs, lam_trans) =
    2.15                !meth
    2.16 -              |> Outer_Syntax.scan Position.start
    2.17 +              |> Outer_Syntax.scan (Keyword.get_lexicons ()) Position.start
    2.18                |> filter Token.is_proper |> tl
    2.19                |> Metis_Tactic.parse_metis_options |> fst
    2.20                |>> the_default [ATP_Proof_Reconstruct.partial_typesN]
     3.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Aug 12 18:54:53 2014 +0200
     3.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Aug 12 20:18:27 2014 +0200
     3.3 @@ -221,7 +221,7 @@
     3.4  
     3.5      val thy = Proof_Context.theory_of lthy
     3.6      val dummy_thm = Thm.transfer thy Drule.dummy_thm
     3.7 -    val pointer = Outer_Syntax.scan Position.none bundle_name
     3.8 +    val pointer = Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none bundle_name
     3.9      val restore_lifting_att = 
    3.10        ([dummy_thm], [Args.src ("Lifting.lifting_restore_internal", Position.none) pointer])
    3.11    in
     4.1 --- a/src/HOL/Tools/try0.ML	Tue Aug 12 18:54:53 2014 +0200
     4.2 +++ b/src/HOL/Tools/try0.ML	Tue Aug 12 20:18:27 2014 +0200
     4.3 @@ -48,12 +48,12 @@
     4.4        NONE
     4.5    end;
     4.6  
     4.7 -val parse_method =
     4.8 -  enclose "(" ")"
     4.9 -  #> Outer_Syntax.scan Position.start
    4.10 -  #> filter Token.is_proper
    4.11 -  #> Scan.read Token.stopper Method.parse
    4.12 -  #> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source");
    4.13 +fun parse_method s =
    4.14 +  enclose "(" ")" s
    4.15 +  |> Outer_Syntax.scan (Keyword.get_lexicons ()) Position.start
    4.16 +  |> filter Token.is_proper
    4.17 +  |> Scan.read Token.stopper Method.parse
    4.18 +  |> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source");
    4.19  
    4.20  fun apply_named_method_on_first_goal ctxt =
    4.21    parse_method
     5.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Aug 12 18:54:53 2014 +0200
     5.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Aug 12 20:18:27 2014 +0200
     5.3 @@ -744,7 +744,7 @@
     5.4  val _ =
     5.5    Outer_Syntax.improper_command @{command_spec "Isabelle.command"} "evaluate nested Isabelle command"
     5.6      (props_text :|-- (fn (pos, str) =>
     5.7 -      (case Outer_Syntax.parse pos str of
     5.8 +      (case Outer_Syntax.parse (Outer_Syntax.get_syntax ()) pos str of
     5.9          [tr] => Scan.succeed (K tr)
    5.10        | _ => Scan.fail_with (K (fn () => "exactly one command expected")))
    5.11        handle ERROR msg => Scan.fail_with (K (fn () => msg))));
     6.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Aug 12 18:54:53 2014 +0200
     6.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Aug 12 20:18:27 2014 +0200
     6.3 @@ -31,9 +31,9 @@
     6.4      (local_theory -> Proof.state) parser -> unit
     6.5    val help_outer_syntax: string list -> unit
     6.6    val print_outer_syntax: unit -> unit
     6.7 -  val scan: Position.T -> string -> Token.T list
     6.8 -  val parse: Position.T -> string -> Toplevel.transition list
     6.9 -  val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
    6.10 +  val scan: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
    6.11 +  val parse: (Scan.lexicon * Scan.lexicon) * outer_syntax ->
    6.12 +    Position.T -> string -> Toplevel.transition list
    6.13    val parse_spans: Token.T list -> Command_Span.span list
    6.14    type isar
    6.15    val isar: TextIO.instream -> bool -> isar
    6.16 @@ -258,25 +258,19 @@
    6.17  
    6.18  (* off-line scanning/parsing *)
    6.19  
    6.20 -fun scan pos str =
    6.21 -  Source.of_string str
    6.22 -  |> Symbol.source
    6.23 -  |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
    6.24 -  |> Source.exhaust;
    6.25 -
    6.26 -fun parse pos str =
    6.27 -  Source.of_string str
    6.28 -  |> Symbol.source
    6.29 -  |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
    6.30 -  |> toplevel_source false NONE lookup_commands_dynamic
    6.31 -  |> Source.exhaust;
    6.32 -
    6.33 -fun parse_tokens lexs pos =
    6.34 +fun scan lexs pos =
    6.35    Source.of_string #>
    6.36    Symbol.source #>
    6.37    Token.source {do_recover = SOME false} (K lexs) pos #>
    6.38    Source.exhaust;
    6.39  
    6.40 +fun parse (lexs, syntax) pos str =
    6.41 +  Source.of_string str
    6.42 +  |> Symbol.source
    6.43 +  |> Token.source {do_recover = SOME false} (K lexs) pos
    6.44 +  |> toplevel_source false NONE (K (lookup_commands syntax))
    6.45 +  |> Source.exhaust;
    6.46 +
    6.47  
    6.48  (* parse spans *)
    6.49  
     7.1 --- a/src/Pure/PIDE/document.ML	Tue Aug 12 18:54:53 2014 +0200
     7.2 +++ b/src/Pure/PIDE/document.ML	Tue Aug 12 20:18:27 2014 +0200
     7.3 @@ -318,7 +318,7 @@
     7.4        val span =
     7.5          Lazy.lazy (fn () =>
     7.6            Position.setmp_thread_data (Position.id_only id)
     7.7 -            (fn () => Outer_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id) text) ());
     7.8 +            (fn () => Outer_Syntax.scan (Keyword.get_lexicons ()) (Position.id id) text) ());
     7.9        val _ =
    7.10          Position.setmp_thread_data (Position.id_only id)
    7.11            (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
     8.1 --- a/src/Pure/PIDE/resources.ML	Tue Aug 12 18:54:53 2014 +0200
     8.2 +++ b/src/Pure/PIDE/resources.ML	Tue Aug 12 20:18:27 2014 +0200
     8.3 @@ -157,7 +157,7 @@
     8.4      val _ = Thy_Header.define_keywords header;
     8.5  
     8.6      val lexs = Keyword.get_lexicons ();
     8.7 -    val toks = Outer_Syntax.parse_tokens lexs text_pos text;
     8.8 +    val toks = Outer_Syntax.scan lexs text_pos text;
     8.9      val spans = Outer_Syntax.parse_spans toks;
    8.10      val elements = Thy_Syntax.parse_elements spans;
    8.11  
     9.1 --- a/src/Pure/Thy/thy_info.ML	Tue Aug 12 18:54:53 2014 +0200
     9.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Aug 12 20:18:27 2014 +0200
     9.3 @@ -380,7 +380,7 @@
     9.4  
     9.5  fun script_thy pos txt =
     9.6    let
     9.7 -    val trs = Outer_Syntax.parse pos txt;
     9.8 +    val trs = Outer_Syntax.parse (Outer_Syntax.get_syntax ()) pos txt;
     9.9      val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
    9.10      val end_state = fold (Toplevel.command_exception true) trs Toplevel.toplevel;
    9.11    in Toplevel.end_theory end_pos end_state end;
    10.1 --- a/src/Pure/Tools/find_consts.ML	Tue Aug 12 18:54:53 2014 +0200
    10.2 +++ b/src/Pure/Tools/find_consts.ML	Tue Aug 12 20:18:27 2014 +0200
    10.3 @@ -143,7 +143,7 @@
    10.4  in
    10.5  
    10.6  fun read_query pos str =
    10.7 -  Outer_Syntax.scan pos str
    10.8 +  Outer_Syntax.scan (Keyword.get_lexicons ()) pos str
    10.9    |> filter Token.is_proper
   10.10    |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
   10.11    |> #1;
    11.1 --- a/src/Pure/Tools/find_theorems.ML	Tue Aug 12 18:54:53 2014 +0200
    11.2 +++ b/src/Pure/Tools/find_theorems.ML	Tue Aug 12 20:18:27 2014 +0200
    11.3 @@ -528,7 +528,7 @@
    11.4  in
    11.5  
    11.6  fun read_query pos str =
    11.7 -  Outer_Syntax.scan pos str
    11.8 +  Outer_Syntax.scan (Keyword.get_lexicons ()) pos str
    11.9    |> filter Token.is_proper
   11.10    |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
   11.11    |> #1;
    12.1 --- a/src/Tools/Code/code_target.ML	Tue Aug 12 18:54:53 2014 +0200
    12.2 +++ b/src/Tools/Code/code_target.ML	Tue Aug 12 20:18:27 2014 +0200
    12.3 @@ -695,7 +695,7 @@
    12.4    let
    12.5      val ctxt = Proof_Context.init_global (Thy_Info.get_theory thyname);
    12.6      val parse = Scan.read Token.stopper (Parse.!!! code_exprP) o
    12.7 -      (filter Token.is_proper o Outer_Syntax.scan Position.none);
    12.8 +      (filter Token.is_proper o Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none);
    12.9    in case parse cmd_expr
   12.10     of SOME f => (writeln "Now generating code..."; f ctxt)
   12.11      | NONE => error ("Bad directive " ^ quote cmd_expr)