eliminated pointless dynamic keywords (TTY legacy);
authorwenzelm
Wed Nov 05 20:49:30 2014 +0100 (2014-11-05)
changeset 58904f49c4f883c58
parent 58903 38c72f5f6c2e
child 58905 55160ef37e8f
eliminated pointless dynamic keywords (TTY legacy);
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/token.ML
src/Pure/PIDE/resources.ML
src/Pure/Thy/thy_header.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Nov 05 20:20:57 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Nov 05 20:49:30 2014 +0100
     1.3 @@ -127,10 +127,11 @@
     1.4  fun thms_of_name ctxt name =
     1.5    let
     1.6      val get = maps (Proof_Context.get_fact ctxt o fst)
     1.7 +    val keywords = Keyword.get_keywords ()
     1.8    in
     1.9      Source.of_string name
    1.10      |> Symbol.source
    1.11 -    |> Token.source Keyword.get_keywords Position.start
    1.12 +    |> Token.source keywords Position.start
    1.13      |> Token.source_proper
    1.14      |> Source.source Token.stopper (Parse.xthms1 >> get)
    1.15      |> Source.exhaust
     2.1 --- a/src/Pure/Isar/outer_syntax.ML	Wed Nov 05 20:20:57 2014 +0100
     2.2 +++ b/src/Pure/Isar/outer_syntax.ML	Wed Nov 05 20:49:30 2014 +0100
     2.3 @@ -226,13 +226,13 @@
     2.4  fun scan keywords pos =
     2.5    Source.of_string #>
     2.6    Symbol.source #>
     2.7 -  Token.source (K keywords) pos #>
     2.8 +  Token.source keywords pos #>
     2.9    Source.exhaust;
    2.10  
    2.11  fun parse (keywords, syntax) pos str =
    2.12    Source.of_string str
    2.13    |> Symbol.source
    2.14 -  |> Token.source (K keywords) pos
    2.15 +  |> Token.source keywords pos
    2.16    |> commands_source syntax
    2.17    |> Source.exhaust;
    2.18  
     3.1 --- a/src/Pure/Isar/token.ML	Wed Nov 05 20:20:57 2014 +0100
     3.2 +++ b/src/Pure/Isar/token.ML	Wed Nov 05 20:49:30 2014 +0100
     3.3 @@ -79,10 +79,10 @@
     3.4    val pretty_src: Proof.context -> src -> Pretty.T
     3.5    val ident_or_symbolic: string -> bool
     3.6    val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
     3.7 -  val source: (unit -> Keyword.keywords) ->
     3.8 +  val source: Keyword.keywords ->
     3.9      Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
    3.10        (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
    3.11 -  val source_strict: (unit -> Keyword.keywords) ->
    3.12 +  val source_strict: Keyword.keywords ->
    3.13      Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
    3.14        (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
    3.15    type 'a parser = T list -> 'a * T list
    3.16 @@ -561,14 +561,14 @@
    3.17  
    3.18  in
    3.19  
    3.20 -fun source' strict get_keywords =
    3.21 +fun source' strict keywords =
    3.22    let
    3.23 -    val scan_strict = Scan.bulk (fn xs => scan (get_keywords ()) xs);
    3.24 +    val scan_strict = Scan.bulk (scan keywords);
    3.25      val scan = if strict then scan_strict else Scan.recover scan_strict recover;
    3.26    in Source.source Symbol_Pos.stopper scan end;
    3.27  
    3.28 -fun source get pos src = Symbol_Pos.source pos src |> source' false get;
    3.29 -fun source_strict get pos src = Symbol_Pos.source pos src |> source' true get;
    3.30 +fun source keywords pos src = Symbol_Pos.source pos src |> source' false keywords;
    3.31 +fun source_strict keywords pos src = Symbol_Pos.source pos src |> source' true keywords;
    3.32  
    3.33  end;
    3.34  
    3.35 @@ -584,7 +584,7 @@
    3.36  
    3.37  fun read_no_commands keywords scan syms =
    3.38    Source.of_list syms
    3.39 -  |> source' true (K (Keyword.no_command_keywords keywords))
    3.40 +  |> source' true (Keyword.no_command_keywords keywords)
    3.41    |> source_proper
    3.42    |> Source.source stopper (Scan.error (Scan.bulk scan))
    3.43    |> Source.exhaust;
     4.1 --- a/src/Pure/PIDE/resources.ML	Wed Nov 05 20:20:57 2014 +0100
     4.2 +++ b/src/Pure/PIDE/resources.ML	Wed Nov 05 20:49:30 2014 +0100
     4.3 @@ -147,8 +147,9 @@
     4.4    let
     4.5      val {name = (name, _), ...} = header;
     4.6      val _ = Thy_Header.define_keywords header;
     4.7 +    val keywords = Keyword.get_keywords ();
     4.8  
     4.9 -    val toks = Outer_Syntax.scan (Keyword.get_keywords ()) text_pos text;
    4.10 +    val toks = Outer_Syntax.scan keywords text_pos text;
    4.11      val spans = Outer_Syntax.parse_spans toks;
    4.12      val elements = Thy_Syntax.parse_elements spans;
    4.13  
     5.1 --- a/src/Pure/Thy/thy_header.ML	Wed Nov 05 20:20:57 2014 +0100
     5.2 +++ b/src/Pure/Thy/thy_header.ML	Wed Nov 05 20:49:30 2014 +0100
     5.3 @@ -141,7 +141,7 @@
     5.4    str
     5.5    |> Source.of_string_limited 8000
     5.6    |> Symbol.source
     5.7 -  |> Token.source_strict (K header_keywords) pos;
     5.8 +  |> Token.source_strict header_keywords pos;
     5.9  
    5.10  fun read_source pos source =
    5.11    let val res =