# HG changeset patch
# User wenzelm
# Date 1347271228 -7200
# Node ID e28b5d8f5613b2851a701808a377e131c1bc1a90
# Parent  fd11fe9dc6bb0ed4ed0d40131efeb167829febd9
more explicit indication of legacy features;

diff -r fd11fe9dc6bb -r e28b5d8f5613 src/Pure/System/build.ML
--- a/src/Pure/System/build.ML	Mon Sep 10 09:57:21 2012 +0200
+++ b/src/Pure/System/build.ML	Mon Sep 10 12:00:28 2012 +0200
@@ -71,6 +71,12 @@
         (case duplicates (op =) (map fst document_variants) of
           [] => ()
         | dups => error ("Duplicate document variants: " ^ commas_quote dups));
+
+      val _ =
+        if Options.string options "document_dump" = "" then ()
+        else
+          Output.physical_stderr
+            "### Legacy feature: old option \"document_dump\" -- use \"document_output\" instead\n";
       val _ =
         Session.init do_output false
           (Options.bool options "browser_info") browser_info
diff -r fd11fe9dc6bb -r e28b5d8f5613 src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Mon Sep 10 09:57:21 2012 +0200
+++ b/src/Pure/System/session.ML	Mon Sep 10 12:00:28 2012 +0200
@@ -121,7 +121,9 @@
     name dump rpath level timing verbose max_threads trace_threads
     parallel_proofs parallel_proofs_threshold =
   ((fn () =>
-     (init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name
+     (Output.physical_stderr
+        "### Legacy feature: old \"isabelle usedir\" -- use \"isabelle build\" instead!\n";
+      init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name
         (doc_dump dump) rpath verbose;
       with_timing item timing use root;
       finish ()))