# HG changeset patch
# User wenzelm
# Date 1271410748 -7200
# Node ID 823c9400eb62c6d4bc6b5c5d28e096704fe9e461
# Parent  0bd034a80a9a7e9b318f1214ef148fbcfc96b0ff
proper checking of ML functors (in Poly/ML 5.2 or later);
eliminated pathetic comments;

diff -r 0bd034a80a9a -r 823c9400eb62 doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Fri Apr 16 10:52:10 2010 +0200
+++ b/doc-src/antiquote_setup.ML	Fri Apr 16 11:39:08 2010 +0200
@@ -54,7 +54,7 @@
 
 fun ml_structure (txt, _) = "functor XXX() = struct structure XX = " ^ txt ^ " end;";
 
-fun ml_functor _ = "";  (*no check!*)
+fun ml_functor (txt, _) = "ML_Env.check_functor " ^ ML_Syntax.print_string txt;
 
 fun index_ml name kind ml = ThyOutput.antiquotation name
   (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) ""))
diff -r 0bd034a80a9a -r 823c9400eb62 src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Fri Apr 16 10:52:10 2010 +0200
+++ b/src/Pure/ML/ml_env.ML	Fri Apr 16 11:39:08 2010 +0200
@@ -9,6 +9,7 @@
   val inherit: Context.generic -> Context.generic -> Context.generic
   val name_space: ML_Name_Space.T
   val local_context: use_context
+  val check_functor: string -> unit
 end
 
 structure ML_Env: ML_ENV =
@@ -88,5 +89,11 @@
   print = writeln,
   error = error};
 
+val is_functor = is_some o #lookupFunct name_space;
+
+fun check_functor name =
+  if is_functor "Table" (*lookup actually works*) andalso is_functor name then ()
+  else error ("Unknown ML functor: " ^ quote name);
+
 end;
 
diff -r 0bd034a80a9a -r 823c9400eb62 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Fri Apr 16 10:52:10 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML	Fri Apr 16 11:39:08 2010 +0200
@@ -599,7 +599,7 @@
 val _ = ml_text "ML" (fn txt => "fn _ => (" ^ txt ^ ");");
 val _ = ml_text "ML_type" (fn txt => "val _ = NONE : (" ^ txt ^ ") option;");
 val _ = ml_text "ML_struct" (fn txt => "functor XXX() = struct structure XX = " ^ txt ^ " end;");
-val _ = ml_text "ML_functor" (K "");  (*no check!*)
+val _ = ml_text "ML_functor" (fn txt => "ML_Env.check_functor " ^ ML_Syntax.print_string txt);
 val _ = ml_text "ML_text" (K "");
 
 end;