src/Pure/Tools/build.scala
changeset 62508 d0b68218ea55
parent 62490 39d01eaf5292
child 62569 5db10482f4cf
     1.1 --- a/src/Pure/Tools/build.scala	Thu Mar 03 21:35:16 2016 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Thu Mar 03 21:59:21 2016 +0100
     1.3 @@ -54,7 +54,7 @@
     1.4      def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
     1.5    }
     1.6  
     1.7 -  def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
     1.8 +  def is_pure(name: String): Boolean = name == "Pure"
     1.9  
    1.10    def session_info(options: Options, select: Boolean, dir: Path,
    1.11        chapter: String, entry: Session_Entry): (String, Session_Info) =
    1.12 @@ -581,33 +581,13 @@
    1.13        """
    1.14        . "$ISABELLE_HOME/lib/scripts/timestart.bash"
    1.15        """ +
    1.16 -      (if (is_pure(name)) {
    1.17 -        val ml_system = Isabelle_System.getenv("ML_SYSTEM")
    1.18 -        val ml_system_base = Library.space_explode('-', ml_system).headOption getOrElse ml_system
    1.19 -        val ml_root =
    1.20 -          List(ml_system, ml_system_base).map(a => "RAW/ROOT_" + a + ".ML").
    1.21 -            find(b => Path.explode("~~/src/Pure/" + b).file.isFile) getOrElse
    1.22 -            error("Missing compatibility file for ML system " + quote(ml_system))
    1.23 -
    1.24 -        if (name == "RAW") {
    1.25 -          """
    1.26 -            rm -f "$OUTPUT"
    1.27 -            "$ISABELLE_PROCESS" \
    1.28 -              -e 'use """ + quote(ml_root) + """ handle _ => OS.Process.exit OS.Process.failure;' \
    1.29 -              -e "ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\";" \
    1.30 -              -q RAW_ML_SYSTEM
    1.31 -          """
    1.32 -        }
    1.33 -        else {
    1.34 -          """
    1.35 -            rm -f "$OUTPUT"
    1.36 -            "$ISABELLE_PROCESS" \
    1.37 -              -e '(use """ + quote(ml_root) + """; use "ROOT.ML") handle _ => OS.Process.exit OS.Process.failure;' \
    1.38 -              -e "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default (); Session.shutdown (); ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\"));" \
    1.39 -              -q RAW_ML_SYSTEM
    1.40 -          """
    1.41 -        }
    1.42 -      }
    1.43 +      (if (is_pure(name))
    1.44 +        """
    1.45 +          rm -f "$OUTPUT"
    1.46 +          "$ISABELLE_PROCESS" -f "ROOT.ML" \
    1.47 +            -e "Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default (); Session.shutdown (); ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\"));" \
    1.48 +            -q RAW_ML_SYSTEM
    1.49 +        """
    1.50        else
    1.51          """
    1.52          rm -f "$OUTPUT"