# HG changeset patch
# User wenzelm
# Date 1540997612 -3600
# Node ID 1a52baa70aed63c44e8ab1d28fbc5cac7cda0ba9
# Parent  ab94035ba6ea58d83e7450b080cc3edbfa8bfa69
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);

diff -r ab94035ba6ea -r 1a52baa70aed NEWS
--- a/NEWS	Wed Oct 31 15:50:45 2018 +0100
+++ b/NEWS	Wed Oct 31 15:53:32 2018 +0100
@@ -15,6 +15,10 @@
 * Infix operators that begin or end with a "*" can now be paranthesized
 without additional spaces, eg "(*)" instead of "( * )".
 
+* ML setup commands (e.g. 'setup', 'method_setup', 'parse_translation')
+need to provide a closed expression -- without trailing semicolon. Minor
+INCOMPATIBILITY.
+
 
 *** Isabelle/jEdit Prover IDE ***
 
diff -r ab94035ba6ea -r 1a52baa70aed src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Wed Oct 31 15:50:45 2018 +0100
+++ b/src/HOL/Deriv.thy	Wed Oct 31 15:53:32 2018 +0100
@@ -62,7 +62,7 @@
         fn context =>
           Named_Theorems.get (Context.proof_of context) @{named_theorems derivative_intros}
           |> map_filter eq_rule)
-  end;
+  end
 \<close>
 
 text \<open>
diff -r ab94035ba6ea -r 1a52baa70aed src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Wed Oct 31 15:50:45 2018 +0100
+++ b/src/HOL/Divides.thy	Wed Oct 31 15:53:32 2018 +0100
@@ -1278,7 +1278,7 @@
       fun prepare_simpset ctxt = HOL_ss |> Simplifier.simpset_map ctxt
         (Simplifier.add_cong if_cong #> fold Simplifier.add_simp simps)
     in fn ctxt => successful_rewrite (Simplifier.put_simpset (prepare_simpset ctxt) ctxt) end
-  end;
+  end
 \<close>
 
 
diff -r ab94035ba6ea -r 1a52baa70aed src/HOL/Eisbach/Tests.thy
--- a/src/HOL/Eisbach/Tests.thy	Wed Oct 31 15:50:45 2018 +0100
+++ b/src/HOL/Eisbach/Tests.thy	Wed Oct 31 15:53:32 2018 +0100
@@ -530,7 +530,7 @@
   Args.term -- Args.term --
   (Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thms) >>
     (fn ((x, y), r) => fn ctxt =>
-      Method_Closure.apply_method ctxt @{method test_method} [x, y] [r] [] ctxt);
+      Method_Closure.apply_method ctxt @{method test_method} [x, y] [r] [] ctxt)
 \<close>
 
 lemma
diff -r ab94035ba6ea -r 1a52baa70aed src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Wed Oct 31 15:50:45 2018 +0100
+++ b/src/HOL/Groups.thy	Wed Oct 31 15:53:32 2018 +0100
@@ -182,7 +182,7 @@
         Syntax.const @{syntax_const "_constrain"} $ Syntax.const c $
           Syntax_Phases.term_of_typ ctxt T
       else raise Match);
-  in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
+  in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end
 \<close> \<comment> \<open>show types that are presumably too general\<close>
 
 class plus =
diff -r ab94035ba6ea -r 1a52baa70aed src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Oct 31 15:50:45 2018 +0100
+++ b/src/HOL/HOL.thy	Wed Oct 31 15:53:32 2018 +0100
@@ -1231,7 +1231,7 @@
             SOME thm => SOME (thm RS neq_to_EQ_False)
           | NONE => NONE)
        | _ => NONE);
-  in proc end;
+  in proc end
 \<close>
 
 simproc_setup let_simp ("Let x f") = \<open>
diff -r ab94035ba6ea -r 1a52baa70aed src/HOL/HOLCF/Cfun.thy
--- a/src/HOL/HOLCF/Cfun.thy	Wed Oct 31 15:50:45 2018 +0100
+++ b/src/HOL/HOLCF/Cfun.thy	Wed Oct 31 15:53:32 2018 +0100
@@ -35,7 +35,7 @@
 
 parse_translation \<open>
 (* rewrite (_cabs x t) => (Abs_cfun (%x. t)) *)
-  [Syntax_Trans.mk_binder_tr (@{syntax_const "_cabs"}, @{const_syntax Abs_cfun})];
+  [Syntax_Trans.mk_binder_tr (@{syntax_const "_cabs"}, @{const_syntax Abs_cfun})]
 \<close>
 
 print_translation \<open>
@@ -60,7 +60,7 @@
           Ast.fold_ast_p @{syntax_const "_cabs"}
             (Ast.unfold_ast @{syntax_const "_cargs"} (Ast.strip_positions pats), body)
       | Lambda_ast_tr asts = raise Ast.AST ("Lambda_ast_tr", asts);
-  in [(@{syntax_const "_Lambda"}, K Lambda_ast_tr)] end;
+  in [(@{syntax_const "_Lambda"}, K Lambda_ast_tr)] end
 \<close>
 
 print_ast_translation \<open>
diff -r ab94035ba6ea -r 1a52baa70aed src/HOL/HOLCF/ex/Pattern_Match.thy
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Wed Oct 31 15:50:45 2018 +0100
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Wed Oct 31 15:53:32 2018 +0100
@@ -132,7 +132,7 @@
 (* rewrite (_pat x) => (succeed) *)
 (* rewrite (_variable x t) => (Abs_cfun (%x. t)) *)
  [(@{syntax_const "_pat"}, fn _ => fn _ => Syntax.const @{const_syntax Fixrec.succeed}),
-  Syntax_Trans.mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_cfun})];
+  Syntax_Trans.mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_cfun})]
 \<close>
 
 text \<open>Printing Case expressions\<close>
@@ -164,7 +164,7 @@
               (Syntax.const @{syntax_const "_match"} $ p $ v) $ t
           end;
 
-  in [(@{const_syntax Rep_cfun}, K Case1_tr')] end;
+  in [(@{const_syntax Rep_cfun}, K Case1_tr')] end
 \<close>
 
 translations
diff -r ab94035ba6ea -r 1a52baa70aed src/HOL/Hoare_Parallel/OG_Syntax.thy
--- a/src/HOL/Hoare_Parallel/OG_Syntax.thy	Wed Oct 31 15:50:45 2018 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy	Wed Oct 31 15:53:32 2018 +0100
@@ -122,7 +122,7 @@
     (@{const_syntax AnnAwait}, K (annbexp_tr' @{syntax_const "_AnnAwait"})),
     (@{const_syntax AnnCond1}, K (annbexp_tr' @{syntax_const "_AnnCond1"})),
     (@{const_syntax AnnCond2}, K (annbexp_tr' @{syntax_const "_AnnCond2"}))]
-  end;
+  end
 \<close>
 
 end
diff -r ab94035ba6ea -r 1a52baa70aed src/HOL/Library/Code_Abstract_Nat.thy
--- a/src/HOL/Library/Code_Abstract_Nat.thy	Wed Oct 31 15:50:45 2018 +0100
+++ b/src/HOL/Library/Code_Abstract_Nat.thy	Wed Oct 31 15:53:32 2018 +0100
@@ -110,7 +110,7 @@
 
   Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc)
 
-end;
+end
 \<close>
 
 end
diff -r ab94035ba6ea -r 1a52baa70aed src/HOL/Library/Code_Lazy.thy
--- a/src/HOL/Library/Code_Lazy.thy	Wed Oct 31 15:50:45 2018 +0100
+++ b/src/HOL/Library/Code_Lazy.thy	Wed Oct 31 15:53:32 2018 +0100
@@ -245,7 +245,7 @@
 ML_file "code_lazy.ML"
 
 setup \<open>
-  Code_Preproc.add_functrans ("lazy_datatype", Code_Lazy.transform_code_eqs);
+  Code_Preproc.add_functrans ("lazy_datatype", Code_Lazy.transform_code_eqs)
 \<close>
 
 end
diff -r ab94035ba6ea -r 1a52baa70aed src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Wed Oct 31 15:50:45 2018 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Wed Oct 31 15:53:32 2018 +0100
@@ -491,7 +491,7 @@
     fun numeral_tr [Free (str, _)] = mk_bintype (the (Int.fromString str))
       | numeral_tr ts = raise TERM ("numeral_tr", ts);
 
-  in [(@{syntax_const "_NumeralType"}, K numeral_tr)] end;
+  in [(@{syntax_const "_NumeralType"}, K numeral_tr)] end
 \<close>
 
 print_translation \<open>
@@ -517,7 +517,7 @@
   in
    [(@{type_syntax bit0}, K (bit_tr' 0)),
     (@{type_syntax bit1}, K (bit_tr' 1))]
-  end;
+  end
 \<close>
 
 subsection \<open>Examples\<close>
diff -r ab94035ba6ea -r 1a52baa70aed src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Oct 31 15:50:45 2018 +0100
+++ b/src/HOL/Set.thy	Wed Oct 31 15:53:32 2018 +0100
@@ -287,7 +287,7 @@
         val exP = ex_tr ctxt [idts, P];
       in Syntax.const @{const_syntax Collect} $ absdummy dummyT exP end;
 
-  in [(@{syntax_const "_Setcompr"}, setcompr_tr)] end;
+  in [(@{syntax_const "_Setcompr"}, setcompr_tr)] end
 \<close>
 
 print_translation \<open>
@@ -326,7 +326,7 @@
           | _ => M
         end
     end;
-  in [(@{const_syntax Collect}, setcompr_tr')] end;
+  in [(@{const_syntax Collect}, setcompr_tr')] end
 \<close>
 
 simproc_setup defined_Bex ("\<exists>x\<in>A. P x \<and> Q x") = \<open>
diff -r ab94035ba6ea -r 1a52baa70aed src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Wed Oct 31 15:50:45 2018 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Wed Oct 31 15:53:32 2018 +0100
@@ -175,12 +175,12 @@
 
   fun ml_tactic source ctxt =
     let
-      val ctxt' = ctxt |> Context.proof_map
-        (ML_Context.expression ("tactic", Position.thread_data ()) "Proof.context -> tactic"
-          "Context.map_proof (ML_Tactic.set tactic)"
-          (ML_Lex.read "fn ctxt: Proof.context =>" @ ML_Lex.read_source source));
+      val ctxt' = ctxt
+        |> Context.proof_map (ML_Context.expression (Input.pos_of source)
+          (ML_Lex.read "Theory.local_setup (ML_Tactic.set (fn ctxt: Proof.context => (" @
+           ML_Lex.read_source source @ ML_Lex.read ")))"));
     in Data.get ctxt' ctxt end;
-end;
+end
 \<close>
 
 
diff -r ab94035ba6ea -r 1a52baa70aed src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed Oct 31 15:50:45 2018 +0100
+++ b/src/Pure/Isar/attrib.ML	Wed Oct 31 15:53:32 2018 +0100
@@ -214,12 +214,11 @@
 fun setup binding scan comment = define_global binding (attribute_syntax scan) comment #> snd;
 fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd;
 
-fun attribute_setup (name, pos) source comment =
-  ML_Lex.read_source source
-  |> ML_Context.expression ("parser", pos) "Thm.attribute context_parser"
-    ("Context.map_proof (Attrib.local_setup " ^
-      ML_Syntax.atomic (ML_Syntax.make_binding (name, pos)) ^
-      " parser " ^ ML_Syntax.print_string comment ^ ")")
+fun attribute_setup binding source comment =
+  ML_Context.expression (Input.pos_of source)
+    (ML_Lex.read
+      ("Theory.local_setup (Attrib.local_setup (" ^ ML_Syntax.make_binding binding ^ ") (") @
+     ML_Lex.read_source source @ ML_Lex.read (") " ^ ML_Syntax.print_string comment ^ ")"))
   |> Context.proof_map;
 
 
diff -r ab94035ba6ea -r 1a52baa70aed src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Oct 31 15:50:45 2018 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Oct 31 15:53:32 2018 +0100
@@ -51,53 +51,46 @@
 (* generic setup *)
 
 fun setup source =
-  ML_Lex.read_source source
-  |> ML_Context.expression ("setup", Position.thread_data ()) "theory -> theory"
-    "Context.map_theory setup"
+  ML_Context.expression (Input.pos_of source)
+    (ML_Lex.read "Theory.setup (" @ ML_Lex.read_source source @ ML_Lex.read ")")
   |> Context.theory_map;
 
 fun local_setup source =
-  ML_Lex.read_source source
-  |> ML_Context.expression ("local_setup", Position.thread_data ()) "local_theory -> local_theory"
-    "Context.map_proof local_setup"
+  ML_Context.expression (Input.pos_of source)
+    (ML_Lex.read "Theory.local_setup (" @ ML_Lex.read_source source @ ML_Lex.read ")")
   |> Context.proof_map;
 
 
 (* translation functions *)
 
 fun parse_ast_translation source =
-  ML_Lex.read_source source
-  |> ML_Context.expression ("parse_ast_translation", Position.thread_data ())
-    "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
-    "Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
+  ML_Context.expression (Input.pos_of source)
+    (ML_Lex.read "Theory.setup (Sign.parse_ast_translation (" @
+      ML_Lex.read_source source @ ML_Lex.read "))")
   |> Context.theory_map;
 
 fun parse_translation source =
-  ML_Lex.read_source source
-  |> ML_Context.expression ("parse_translation", Position.thread_data ())
-    "(string * (Proof.context -> term list -> term)) list"
-    "Context.map_theory (Sign.parse_translation parse_translation)"
+  ML_Context.expression (Input.pos_of source)
+    (ML_Lex.read "Theory.setup (Sign.parse_translation (" @
+      ML_Lex.read_source source @ ML_Lex.read "))")
   |> Context.theory_map;
 
 fun print_translation source =
-  ML_Lex.read_source source
-  |> ML_Context.expression ("print_translation", Position.thread_data ())
-    "(string * (Proof.context -> term list -> term)) list"
-    "Context.map_theory (Sign.print_translation print_translation)"
+  ML_Context.expression (Input.pos_of source)
+    (ML_Lex.read "Theory.setup (Sign.print_translation (" @
+      ML_Lex.read_source source @ ML_Lex.read "))")
   |> Context.theory_map;
 
 fun typed_print_translation source =
-  ML_Lex.read_source source
-  |> ML_Context.expression ("typed_print_translation", Position.thread_data ())
-    "(string * (Proof.context -> typ -> term list -> term)) list"
-    "Context.map_theory (Sign.typed_print_translation typed_print_translation)"
+  ML_Context.expression (Input.pos_of source)
+    (ML_Lex.read "Theory.setup (Sign.typed_print_translation (" @
+      ML_Lex.read_source source @ ML_Lex.read "))")
   |> Context.theory_map;
 
 fun print_ast_translation source =
-  ML_Lex.read_source source
-  |> ML_Context.expression ("print_ast_translation", Position.thread_data ())
-    "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
-    "Context.map_theory (Sign.print_ast_translation print_ast_translation)"
+  ML_Context.expression (Input.pos_of source)
+    (ML_Lex.read "Theory.setup (Sign.print_ast_translation (" @
+      ML_Lex.read_source source @ ML_Lex.read "))")
   |> Context.theory_map;
 
 
@@ -142,22 +135,22 @@
 (* declarations *)
 
 fun declaration {syntax, pervasive} source =
-  ML_Lex.read_source source
-  |> ML_Context.expression ("declaration", Position.thread_data ()) "Morphism.declaration"
-    ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
-      \pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
+  ML_Context.expression (Input.pos_of source)
+    (ML_Lex.read
+      ("Theory.local_setup (Local_Theory.declaration {syntax = " ^
+        Bool.toString syntax ^ ", pervasive = " ^ Bool.toString pervasive ^ "} (") @
+     ML_Lex.read_source source @ ML_Lex.read "))")
   |> Context.proof_map;
 
 
 (* simprocs *)
 
 fun simproc_setup name lhss source =
-  ML_Lex.read_source source
-  |> ML_Context.expression ("proc", Position.thread_data ())
-    "Morphism.morphism -> Proof.context -> cterm -> thm option"
-    ("Context.map_proof (Simplifier.define_simproc_cmd " ^
-      ML_Syntax.atomic (ML_Syntax.make_binding name) ^
-      "{lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc})")
+  ML_Context.expression (Input.pos_of source)
+    (ML_Lex.read
+      ("Theory.local_setup (Simplifier.define_simproc_cmd (" ^
+        ML_Syntax.make_binding name ^ ") {lhss = " ^ ML_Syntax.print_strings lhss ^
+        ", proc = (") @ ML_Lex.read_source source @ ML_Lex.read ")})")
   |> Context.proof_map;
 
 
diff -r ab94035ba6ea -r 1a52baa70aed src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Oct 31 15:50:45 2018 +0100
+++ b/src/Pure/Isar/method.ML	Wed Oct 31 15:53:32 2018 +0100
@@ -368,13 +368,12 @@
   Scan.state :|-- (fn context =>
     Scan.lift (Args.text_declaration (fn source =>
       let
-        val context' = context |>
-          ML_Context.expression ("tactic", Position.thread_data ())
-            "Morphism.morphism -> thm list -> tactic"
-            "Method.set_tactic tactic"
-            (ML_Lex.read "fn morphism: Morphism.morphism => fn facts: thm list =>" @
-             ML_Lex.read_source source);
-        val tac = the_tactic context';
+        val tac =
+          context
+          |> ML_Context.expression (Input.pos_of source)
+              (ML_Lex.read "Context.>> (Method.set_tactic (fn morphism: Morphism.morphism => fn facts: thm list => (" @
+               ML_Lex.read_source source @ ML_Lex.read ")))")
+          |> the_tactic;
       in
         fn phi => set_tactic (fn _ => Context.setmp_generic_context (SOME context) (tac phi))
       end)) >> (fn decl => Morphism.form (the_tactic (Morphism.form decl context))));
@@ -475,13 +474,11 @@
 fun setup binding scan comment = define_global binding (method_syntax scan) comment #> snd;
 fun local_setup binding scan comment = define binding (method_syntax scan) comment #> snd;
 
-fun method_setup (name, pos) source comment =
-  ML_Lex.read_source source
-  |> ML_Context.expression ("parser", pos)
-    "(Proof.context -> Proof.method) context_parser"
-    ("Context.map_proof (Method.local_setup " ^
-      ML_Syntax.atomic (ML_Syntax.make_binding (name, pos)) ^
-      " parser " ^ ML_Syntax.print_string comment ^ ")")
+fun method_setup binding source comment =
+  ML_Context.expression (Input.pos_of source)
+    (ML_Lex.read
+      ("Theory.local_setup (Method.local_setup (" ^ ML_Syntax.make_binding binding ^ ") (") @
+     ML_Lex.read_source source @ ML_Lex.read (")" ^ ML_Syntax.print_string comment ^ ")"))
   |> Context.proof_map;
 
 
diff -r ab94035ba6ea -r 1a52baa70aed src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Wed Oct 31 15:50:45 2018 +0100
+++ b/src/Pure/ML/ml_context.ML	Wed Oct 31 15:53:32 2018 +0100
@@ -21,8 +21,8 @@
     ML_Lex.token Antiquote.antiquote list -> unit
   val eval_source_in: Proof.context option -> ML_Compiler.flags -> Input.source -> unit
   val exec: (unit -> unit) -> Context.generic -> Context.generic
-  val expression: string * Position.T -> string -> string ->
-    ML_Lex.token Antiquote.antiquote list -> Context.generic -> Context.generic
+  val expression: Position.T -> ML_Lex.token Antiquote.antiquote list ->
+    Context.generic -> Context.generic
 end
 
 structure ML_Context: ML_CONTEXT =
@@ -214,13 +214,7 @@
     SOME context' => context'
   | NONE => error "Missing context after execution");
 
-fun expression (name, pos) constraint body ants =
-  exec (fn () =>
-    eval ML_Compiler.flags pos
-     (ML_Lex.read "Context.put_generic_context (SOME (let val " @
-       ML_Lex.read_set_range (Position.range_of_properties (Position.properties_of pos)) name @
-      ML_Lex.read (": " ^ constraint ^ " =") @ ants @
-      ML_Lex.read ("in " ^ body ^ " end (Context.the_generic_context ())));")));
+fun expression pos ants = exec (fn () => eval ML_Compiler.flags pos ants);
 
 end;
 
diff -r ab94035ba6ea -r 1a52baa70aed src/Pure/Tools/ghc.ML
--- a/src/Pure/Tools/ghc.ML	Wed Oct 31 15:50:45 2018 +0100
+++ b/src/Pure/Tools/ghc.ML	Wed Oct 31 15:53:32 2018 +0100
@@ -119,9 +119,9 @@
     (antiquotation \<^binding>\<open>cartouche\<close> (Scan.lift Args.cartouche_input)
       (fn {context = ctxt, argument, ...} =>
         ctxt |> Context.proof_map
-          (ML_Context.expression ("result", Position.thread_data ())
-            "string" "Context.map_proof (GHC.set_result result)"
-            (ML_Lex.read_source argument))
+          (ML_Context.expression (Input.pos_of argument)
+            (ML_Lex.read "Theory.local_setup (GHC.set_result (" @
+             ML_Lex.read_source argument @ ML_Lex.read "))"))
         |> the_result |> print_string));
 
 end;