added "document_dump_only" (cf. negated usedir -C);
authorwenzelm
Tue Jul 24 12:20:01 2012 +0200 (2012-07-24)
changeset 484687f2998b95249
parent 48467 a4318c36a829
child 48469 826a771cff33
added "document_dump_only" (cf. negated usedir -C);
etc/options
src/Pure/System/build.ML
     1.1 --- a/etc/options	Tue Jul 24 12:14:16 2012 +0200
     1.2 +++ b/etc/options	Tue Jul 24 12:20:01 2012 +0200
     1.3 @@ -7,6 +7,7 @@
     1.4  declare document_variants : string = "outline=/proof,/ML"
     1.5  declare document_graph : bool = false
     1.6  declare document_dump : string = ""
     1.7 +declare document_dump_only : bool = false
     1.8  declare no_document : bool = false
     1.9  
    1.10  declare threads : int = 0
     2.1 --- a/src/Pure/System/build.ML	Tue Jul 24 12:14:16 2012 +0200
     2.2 +++ b/src/Pure/System/build.ML	Tue Jul 24 12:20:01 2012 +0200
     2.3 @@ -55,14 +55,11 @@
     2.4          (Options.bool options "document_graph")
     2.5          (space_explode ":" (Options.string options "document_variants"))
     2.6          parent base_name
     2.7 -        (true (* FIXME copy document/ files on Scala side!? *),
     2.8 -          Options.string options "document_dump")
     2.9 +        (not (Options.bool options "document_dump_only"), Options.string options "document_dump")
    2.10          (Options.string options "browser_info_remote")
    2.11          verbose;
    2.12 -
    2.13      val _ = Session.with_timing name timing (List.app use_theories) theories;
    2.14      val _ = Session.finish ();
    2.15 -
    2.16      val _ = if save then () else quit ();
    2.17    in () end
    2.18    handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);