clarified modules;
authorwenzelm
Mon, 04 Apr 2016 15:35:24 +0200
changeset 62845 31177a9c3025
parent 62844 eeea384cafc8
child 62846 3c576c7f9731
clarified modules;
Admin/lib/Tools/makedist
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/ROOT.scala
src/Pure/System/distribution.ML
src/Pure/System/distribution.scala
src/Pure/build-jars
--- a/Admin/lib/Tools/makedist	Mon Apr 04 14:53:30 2016 +0200
+++ b/Admin/lib/Tools/makedist	Mon Apr 04 15:35:24 2016 +0200
@@ -159,12 +159,13 @@
 perl -pi \
   -e "s,val is_identified = false,val is_identified = true,g;" \
   -e "s,val is_official = false,val is_official = ${IS_OFFICIAL},g;" \
-  src/Pure/ROOT.ML src/Pure/ROOT.scala
+  src/Pure/System/distribution.ML src/Pure/System/distribution.scala
 
 perl -pi -e "s,ISABELLE_ID=\"\",ISABELLE_ID=\"$IDENT\",g" lib/scripts/getsettings
 perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings
 perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template
-perl -pi -e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML src/Pure/ROOT.scala lib/Tools/version
+perl -pi -e "s,unidentified repository version,$DISTVERSION,g" \
+  src/Pure/System/distribution.ML src/Pure/System/distribution.scala lib/Tools/version
 perl -pi -e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README
 
 mkdir -p contrib
--- a/src/Pure/ROOT	Mon Apr 04 14:53:30 2016 +0200
+++ b/src/Pure/ROOT	Mon Apr 04 15:35:24 2016 +0200
@@ -154,6 +154,7 @@
     "System/bash.ML"
     "System/bash_windows.ML"
     "System/command_line.ML"
+    "System/distribution.ML"
     "System/invoke_scala.ML"
     "System/isabelle_process.ML"
     "System/isabelle_system.ML"
--- a/src/Pure/ROOT.ML	Mon Apr 04 14:53:30 2016 +0200
+++ b/src/Pure/ROOT.ML	Mon Apr 04 15:35:24 2016 +0200
@@ -11,13 +11,6 @@
 if List.exists (fn (a, _) => a = "FixedInt") (#allStruct ML_Name_Space.global ()) then ()
 else use "ML/fixed_int_dummy.ML";
 
-structure Distribution =     (*filled-in by makedist*)
-struct
-  val version = "unidentified repository version";
-  val is_identified = false;
-  val is_official = false;
-end;
-
 
 (* multithreading *)
 
@@ -29,6 +22,8 @@
 
 (* ML system *)
 
+use "System/distribution.ML";
+
 use "ML/ml_heap.ML";
 use "ML/ml_profiling.ML";
 use "ML/ml_pretty.ML";
@@ -291,6 +286,7 @@
 else use "System/bash.ML";
 use "System/isabelle_system.ML";
 
+
 (*theory documents*)
 use "Thy/term_style.ML";
 use "Isar/outer_syntax.ML";
--- a/src/Pure/ROOT.scala	Mon Apr 04 14:53:30 2016 +0200
+++ b/src/Pure/ROOT.scala	Mon Apr 04 15:35:24 2016 +0200
@@ -7,13 +7,6 @@
 
 package object isabelle
 {
-  object Distribution     /*filled-in by makedist*/
-  {
-    val version = "unidentified repository version"
-    val is_identified = false
-    val is_official = false
-  }
-
   val ERROR = Exn.ERROR
   val error = Exn.error _
   val cat_error = Exn.cat_error _
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/distribution.ML	Mon Apr 04 15:35:24 2016 +0200
@@ -0,0 +1,12 @@
+(*  Title:      Pure/System/distribution.ML
+    Author:     Makarius
+
+The Isabelle system distribution -- filled-in by makedist.
+*)
+
+structure Distribution =
+struct
+  val version = "unidentified repository version";
+  val is_identified = false;
+  val is_official = false;
+end;
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/distribution.scala	Mon Apr 04 15:35:24 2016 +0200
@@ -0,0 +1,15 @@
+/*  Title:      Pure/System/distribution.scala
+    Author:     Makarius
+
+The Isabelle system distribution -- filled-in by makedist.
+*/
+
+package isabelle
+
+
+object Distribution
+{
+  val version = "unidentified repository version"
+  val is_identified = false
+  val is_official = false
+}
--- a/src/Pure/build-jars	Mon Apr 04 14:53:30 2016 +0200
+++ b/src/Pure/build-jars	Mon Apr 04 15:35:24 2016 +0200
@@ -76,6 +76,7 @@
   System/bash.scala
   System/command_line.scala
   System/cygwin.scala
+  System/distribution.scala
   System/getopts.scala
   System/invoke_scala.scala
   System/isabelle_charset.scala