tuned signature;
authorwenzelm
Sun Nov 30 14:02:48 2014 +0100 (2014-11-30 ago)
changeset 59067dd8ec9138112
parent 59066 45ab32a542fe
child 59068 8606f2ee11b1
tuned signature;
src/Doc/antiquote_setup.ML
src/HOL/ex/Cartouche_Examples.thy
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/method.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_lex.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Doc/antiquote_setup.ML	Sun Nov 30 13:15:04 2014 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Sun Nov 30 14:02:48 2014 +0100
     1.3 @@ -37,28 +37,29 @@
     1.4  
     1.5  local
     1.6  
     1.7 -val ml_toks = ML_Lex.read Position.none;
     1.8 +fun ml_val (toks1, []) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read ");"
     1.9 +  | ml_val (toks1, toks2) =
    1.10 +      ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read ");";
    1.11  
    1.12 -fun ml_val (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks ");"
    1.13 -  | ml_val (toks1, toks2) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : " @ toks2 @ ml_toks ");";
    1.14 -
    1.15 -fun ml_op (toks1, []) = ml_toks "fn _ => (op " @ toks1 @ ml_toks ");"
    1.16 -  | ml_op (toks1, toks2) = ml_toks "fn _ => (op " @ toks1 @ ml_toks " : " @ toks2 @ ml_toks ");";
    1.17 +fun ml_op (toks1, []) = ML_Lex.read "fn _ => (op " @ toks1 @ ML_Lex.read ");"
    1.18 +  | ml_op (toks1, toks2) =
    1.19 +      ML_Lex.read "fn _ => (op " @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read ");";
    1.20  
    1.21 -fun ml_type (toks1, []) = ml_toks "val _ = NONE : (" @ toks1 @ ml_toks ") option;"
    1.22 +fun ml_type (toks1, []) = ML_Lex.read "val _ = NONE : (" @ toks1 @ ML_Lex.read ") option;"
    1.23    | ml_type (toks1, toks2) =
    1.24 -      ml_toks "val _ = [NONE : (" @ toks1 @ ml_toks ") option, NONE : (" @
    1.25 -        toks2 @ ml_toks ") option];";
    1.26 +      ML_Lex.read "val _ = [NONE : (" @ toks1 @ ML_Lex.read ") option, NONE : (" @
    1.27 +        toks2 @ ML_Lex.read ") option];";
    1.28  
    1.29 -fun ml_exception (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : exn);"
    1.30 +fun ml_exception (toks1, []) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : exn);"
    1.31    | ml_exception (toks1, toks2) =
    1.32 -      ml_toks "fn _ => (" @ toks1 @ ml_toks " : " @ toks2 @ ml_toks " -> exn);";
    1.33 +      ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read " -> exn);";
    1.34  
    1.35  fun ml_structure (toks, _) =
    1.36 -  ml_toks "functor XXX() = struct structure XX = " @ toks @ ml_toks " end;";
    1.37 +  ML_Lex.read "functor XXX() = struct structure XX = " @ toks @ ML_Lex.read " end;";
    1.38  
    1.39  fun ml_functor (Antiquote.Text tok :: _, _) =
    1.40 -      ml_toks "ML_Env.check_functor " @ ml_toks (ML_Syntax.print_string (ML_Lex.content_of tok))
    1.41 +      ML_Lex.read "ML_Env.check_functor " @
    1.42 +      ML_Lex.read (ML_Syntax.print_string (ML_Lex.content_of tok))
    1.43    | ml_functor _ = raise Fail "Bad ML functor specification";
    1.44  
    1.45  val is_name = ML_Lex.kind_of #> (fn kind => kind = ML_Lex.Ident orelse kind = ML_Lex.LongIdent);
     2.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Sun Nov 30 13:15:04 2014 +0100
     2.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Sun Nov 30 14:02:48 2014 +0100
     2.3 @@ -142,10 +142,7 @@
     2.4    Thy_Output.antiquotation @{binding ML_cartouche}
     2.5      (Scan.lift Args.cartouche_source_position) (fn {context, ...} => fn source =>
     2.6        let
     2.7 -        val toks =
     2.8 -          ML_Lex.read Position.none "fn _ => (" @
     2.9 -          ML_Lex.read_source false source @
    2.10 -          ML_Lex.read Position.none ");";
    2.11 +        val toks = ML_Lex.read "fn _ => (" @ ML_Lex.read_source false source @ ML_Lex.read ");";
    2.12          val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags (Input.pos_of source) toks;
    2.13        in "" end);
    2.14  *}
    2.15 @@ -215,8 +212,7 @@
    2.16        val ctxt' = ctxt |> Context.proof_map
    2.17          (ML_Context.expression (Input.range_of source) "tactic" "Proof.context -> tactic"
    2.18            "Context.map_proof (ML_Tactic.set tactic)"
    2.19 -          (ML_Lex.read Position.none "fn ctxt: Proof.context =>" @
    2.20 -           ML_Lex.read_source false source));
    2.21 +          (ML_Lex.read "fn ctxt: Proof.context =>" @ ML_Lex.read_source false source));
    2.22      in Data.get ctxt' ctxt end;
    2.23  end;
    2.24  *}
     3.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Nov 30 13:15:04 2014 +0100
     3.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Nov 30 14:02:48 2014 +0100
     3.3 @@ -131,15 +131,13 @@
     3.4      val body_range = Input.range_of source;
     3.5      val body = ML_Lex.read_source false source;
     3.6  
     3.7 -    val hidden = ML_Lex.read Position.none;
     3.8 -    val visible = ML_Lex.read_set_range;
     3.9      val ants =
    3.10 -      hidden
    3.11 +      ML_Lex.read
    3.12         ("local\n\
    3.13          \  val binding = " ^ ML_Syntax.make_binding (name, #1 range) ^ ";\n\
    3.14 -        \  val") @ visible body_range "oracle" @ hidden "=" @ body @ hidden (";\n\
    3.15 -        \in\n\
    3.16 -        \  val") @ visible range name @ hidden "=\
    3.17 +        \  val") @ ML_Lex.read_set_range body_range "oracle" @ ML_Lex.read "=" @ body @
    3.18 +        ML_Lex.read (";\nin\n\
    3.19 +        \  val") @ ML_Lex.read_set_range range name @ ML_Lex.read "=\
    3.20          \ snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, oracle))));\n\
    3.21          \end;\n";
    3.22    in
     4.1 --- a/src/Pure/Isar/method.ML	Sun Nov 30 13:15:04 2014 +0100
     4.2 +++ b/src/Pure/Isar/method.ML	Sun Nov 30 14:02:48 2014 +0100
     4.3 @@ -284,7 +284,7 @@
     4.4            ML_Context.expression (Input.range_of source)
     4.5              "tactic" "Morphism.morphism -> thm list -> tactic"
     4.6              "Method.set_tactic tactic"
     4.7 -            (ML_Lex.read Position.none "fn morphism: Morphism.morphism => fn facts: thm list =>" @
     4.8 +            (ML_Lex.read "fn morphism: Morphism.morphism => fn facts: thm list =>" @
     4.9               ML_Lex.read_source false source);
    4.10          val tac = the_tactic context';
    4.11        in
     5.1 --- a/src/Pure/ML/ml_context.ML	Sun Nov 30 13:15:04 2014 +0100
     5.2 +++ b/src/Pure/ML/ml_context.ML	Sun Nov 30 14:02:48 2014 +0100
     5.3 @@ -170,7 +170,7 @@
     5.4  
     5.5  fun eval_file flags path =
     5.6    let val pos = Path.position path
     5.7 -  in eval flags pos (ML_Lex.read pos (File.read path)) end;
     5.8 +  in eval flags pos (ML_Lex.read_pos pos (File.read path)) end;
     5.9  
    5.10  fun eval_source flags source =
    5.11    eval flags (Input.pos_of source) (ML_Lex.read_source (#SML flags) source);
    5.12 @@ -184,16 +184,11 @@
    5.13      (fn () => eval_source flags source) ();
    5.14  
    5.15  fun expression range name constraint body ants =
    5.16 -  let
    5.17 -    val hidden = ML_Lex.read Position.none;
    5.18 -    val visible = ML_Lex.read_set_range range;
    5.19 -  in
    5.20 -    exec (fn () =>
    5.21 -      eval ML_Compiler.flags (#1 range)
    5.22 -       (hidden "Context.set_thread_data (SOME (let val " @ visible name @
    5.23 -        hidden (": " ^ constraint ^ " =") @ ants @
    5.24 -        hidden ("in " ^ body ^ " end (ML_Context.the_generic_context ())));")))
    5.25 -  end;
    5.26 +  exec (fn () =>
    5.27 +    eval ML_Compiler.flags (#1 range)
    5.28 +     (ML_Lex.read "Context.set_thread_data (SOME (let val " @ ML_Lex.read_set_range range name @
    5.29 +      ML_Lex.read (": " ^ constraint ^ " =") @ ants @
    5.30 +      ML_Lex.read ("in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
    5.31  
    5.32  end;
    5.33  
     6.1 --- a/src/Pure/ML/ml_lex.ML	Sun Nov 30 13:15:04 2014 +0100
     6.2 +++ b/src/Pure/ML/ml_lex.ML	Sun Nov 30 14:02:48 2014 +0100
     6.3 @@ -25,7 +25,8 @@
     6.4      (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
     6.5        Source.source) Source.source
     6.6    val tokenize: string -> token list
     6.7 -  val read: Position.T -> Symbol_Pos.text -> token Antiquote.antiquote list
     6.8 +  val read_pos: Position.T -> Symbol_Pos.text -> token Antiquote.antiquote list
     6.9 +  val read: Symbol_Pos.text -> token Antiquote.antiquote list
    6.10    val read_set_range: Position.range -> Symbol_Pos.text -> token Antiquote.antiquote list
    6.11    val read_source: bool -> Input.source -> token Antiquote.antiquote list
    6.12  end;
    6.13 @@ -324,11 +325,12 @@
    6.14  
    6.15  val tokenize = Source.of_string #> Symbol.source #> source #> Source.exhaust;
    6.16  
    6.17 -val read = gen_read false;
    6.18 +val read_pos = gen_read false;
    6.19 +
    6.20 +val read = read_pos Position.none;
    6.21  
    6.22  fun read_set_range range =
    6.23 -  read Position.none
    6.24 -  #> map (fn Antiquote.Text tok => Antiquote.Text (set_range range tok) | antiq => antiq);
    6.25 +  read #> map (fn Antiquote.Text tok => Antiquote.Text (set_range range tok) | antiq => antiq);
    6.26  
    6.27  fun read_source SML source =
    6.28    let
     7.1 --- a/src/Pure/Thy/thy_output.ML	Sun Nov 30 13:15:04 2014 +0100
     7.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Nov 30 14:02:48 2014 +0100
     7.3 @@ -671,9 +671,7 @@
     7.4      verbatim_text ctxt (Input.source_content source)));
     7.5  
     7.6  fun ml_enclose bg en source =
     7.7 -  ML_Lex.read Position.none bg @
     7.8 -  ML_Lex.read_source false source @
     7.9 -  ML_Lex.read Position.none en;
    7.10 +  ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en;
    7.11  
    7.12  in
    7.13  
    7.14 @@ -686,7 +684,7 @@
    7.15  
    7.16    ml_text @{binding ML_functor}   (* FIXME formal treatment of functor name (!?) *)
    7.17      (fn source =>
    7.18 -      ML_Lex.read Position.none ("ML_Env.check_functor " ^
    7.19 +      ML_Lex.read ("ML_Env.check_functor " ^
    7.20          ML_Syntax.print_string (Input.source_content source))) #>
    7.21  
    7.22    ml_text @{binding ML_text} (K []));