# HG changeset patch
# User wenzelm
# Date 1412769343 -7200
# Node ID 08536219d3a23959d362136b85cc0cc10c25281e
# Parent  41333b45bff92d4aac5c27b9c2df5206ae3c6552
tuned;

diff -r 41333b45bff9 -r 08536219d3a2 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Wed Oct 08 11:50:25 2014 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Wed Oct 08 13:55:43 2014 +0200
@@ -7,6 +7,41 @@
 structure ML_Antiquotations: sig end =
 struct
 
+(* ML support *)
+
+val _ = Theory.setup
+ (ML_Antiquotation.inline @{binding assert}
+    (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
+
+  ML_Antiquotation.inline @{binding make_string} (Scan.succeed ml_make_string) #>
+
+  ML_Antiquotation.declaration @{binding print}
+    (Scan.lift (Scan.optional Args.name "Output.writeln"))
+      (fn src => fn output => fn ctxt =>
+        let
+          val (_, pos) = Token.name_of_src src;
+          val (a, ctxt') = ML_Antiquotation.variant "output" ctxt;
+          val env =
+            "val " ^ a ^ ": string -> unit =\n\
+            \  (" ^ output ^ ") o (fn s => s ^ Position.here (" ^
+            ML_Syntax.print_position pos ^ "));\n";
+          val body =
+            "(fn x => (Isabelle." ^ a ^ " (" ^ ml_make_string ^ " x); x))";
+        in (K (env, body), ctxt') end));
+
+
+(* embedded source *)
+
+val _ = Theory.setup
+ (ML_Antiquotation.value @{binding source}
+    (Scan.lift Args.text_source_position >> (fn {delimited, text, pos} =>
+      "{delimited = " ^ Bool.toString delimited ^
+      ", text = " ^ ML_Syntax.print_string text ^
+      ", pos = " ^ ML_Syntax.print_position pos ^ "}")));
+
+
+(* formal entities *)
+
 val _ = Theory.setup
  (ML_Antiquotation.value @{binding system_option}
     (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
@@ -52,39 +87,6 @@
           ML_Syntax.atomic (ML_Syntax.print_term t))));
 
 
-(* embedded source *)
-
-val _ = Theory.setup
- (ML_Antiquotation.value @{binding source}
-    (Scan.lift Args.text_source_position >> (fn {delimited, text, pos} =>
-      "{delimited = " ^ Bool.toString delimited ^
-      ", text = " ^ ML_Syntax.print_string text ^
-      ", pos = " ^ ML_Syntax.print_position pos ^ "}")));
-
-
-(* ML support *)
-
-val _ = Theory.setup
- (ML_Antiquotation.inline @{binding assert}
-    (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
-
-  ML_Antiquotation.inline @{binding make_string} (Scan.succeed ml_make_string) #>
-
-  ML_Antiquotation.declaration @{binding print}
-    (Scan.lift (Scan.optional Args.name "Output.writeln"))
-      (fn src => fn output => fn ctxt =>
-        let
-          val (_, pos) = Token.name_of_src src;
-          val (a, ctxt') = ML_Antiquotation.variant "output" ctxt;
-          val env =
-            "val " ^ a ^ ": string -> unit =\n\
-            \  (" ^ output ^ ") o (fn s => s ^ Position.here (" ^
-            ML_Syntax.print_position pos ^ "));\n";
-          val body =
-            "(fn x => (Isabelle." ^ a ^ " (" ^ ml_make_string ^ " x); x))";
-        in (K (env, body), ctxt') end));
-
-
 (* type classes *)
 
 fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>