renamed ISABELLE_POLYML to ML_SYSTEM_POLYML, to avoid overlap with ISABELLE_POLYML_PATH;
authorwenzelm
Sun Sep 21 20:22:12 2014 +0200 (2014-09-21)
changeset 5841322dd971f6938
parent 58412 f65f11f4854c
child 58414 f945e7af0d27
child 58415 8392d221bd91
renamed ISABELLE_POLYML to ML_SYSTEM_POLYML, to avoid overlap with ISABELLE_POLYML_PATH;
lib/scripts/getsettings
src/Doc/System/Basics.thy
src/HOL/ROOT
src/Tools/ROOT
     1.1 --- a/lib/scripts/getsettings	Sun Sep 21 20:14:04 2014 +0200
     1.2 +++ b/lib/scripts/getsettings	Sun Sep 21 20:22:12 2014 +0200
     1.3 @@ -260,10 +260,10 @@
     1.4  #build condition etc.
     1.5  case "$ML_SYSTEM" in
     1.6    polyml*)
     1.7 -    ISABELLE_POLYML="true"
     1.8 +    ML_SYSTEM_POLYML="true"
     1.9      ;;
    1.10    *)
    1.11 -    ISABELLE_POLYML=""
    1.12 +    ML_SYSTEM_POLYML=""
    1.13      ;;
    1.14  esac
    1.15  
     2.1 --- a/src/Doc/System/Basics.thy	Sun Sep 21 20:14:04 2014 +0200
     2.2 +++ b/src/Doc/System/Basics.thy	Sun Sep 21 20:22:12 2014 +0200
     2.3 @@ -217,7 +217,7 @@
     2.4    automatically obtained by composing the values of @{setting
     2.5    ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version values.
     2.6  
     2.7 -  \item[@{setting_def ISABELLE_POLYML}@{text "\<^sup>*"}] is @{verbatim true}
     2.8 +  \item[@{setting_def ML_SYSTEM_POLYML}@{text "\<^sup>*"}] is @{verbatim true}
     2.9    for @{setting ML_SYSTEM} values derived from Poly/ML, as opposed to
    2.10    SML/NJ where it is empty.  This is particularly useful with the
    2.11    build option @{system_option condition}
     3.1 --- a/src/HOL/ROOT	Sun Sep 21 20:14:04 2014 +0200
     3.2 +++ b/src/HOL/ROOT	Sun Sep 21 20:22:12 2014 +0200
     3.3 @@ -388,7 +388,7 @@
     3.4    description {*
     3.5      Various decision procedures, typically involving reflection.
     3.6    *}
     3.7 -  options [condition = ISABELLE_POLYML, document = false]
     3.8 +  options [condition = ML_SYSTEM_POLYML, document = false]
     3.9    theories Decision_Procs
    3.10  
    3.11  session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
    3.12 @@ -401,7 +401,7 @@
    3.13    description {*
    3.14      Examples for program extraction in Higher-Order Logic.
    3.15    *}
    3.16 -  options [condition = ISABELLE_POLYML, parallel_proofs = 0]
    3.17 +  options [condition = ML_SYSTEM_POLYML, parallel_proofs = 0]
    3.18    theories [document = false]
    3.19      "~~/src/HOL/Library/Code_Target_Numeral"
    3.20      "~~/src/HOL/Library/Monad_Syntax"
    3.21 @@ -524,7 +524,7 @@
    3.22    description {*
    3.23      Miscellaneous examples for Higher-Order Logic.
    3.24    *}
    3.25 -  options [timeout = 3600, condition = ISABELLE_POLYML]
    3.26 +  options [timeout = 3600, condition = ML_SYSTEM_POLYML]
    3.27    theories [document = false]
    3.28      "~~/src/HOL/Library/State_Monad"
    3.29      Code_Binary_Nat_examples
    3.30 @@ -719,7 +719,7 @@
    3.31    theories Nominal
    3.32  
    3.33  session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
    3.34 -  options [timeout = 3600, condition = ISABELLE_POLYML, document = false]
    3.35 +  options [timeout = 3600, condition = ML_SYSTEM_POLYML, document = false]
    3.36    theories
    3.37      Nominal_Examples_Base
    3.38    theories [condition = ISABELLE_FULL_TEST]
     4.1 --- a/src/Tools/ROOT	Sun Sep 21 20:14:04 2014 +0200
     4.2 +++ b/src/Tools/ROOT	Sun Sep 21 20:22:12 2014 +0200
     4.3 @@ -1,11 +1,11 @@
     4.4  session Spec_Check in Spec_Check = Pure +
     4.5    theories
     4.6      Spec_Check
     4.7 -  theories [condition = ISABELLE_POLYML]
     4.8 +  theories [condition = ML_SYSTEM_POLYML]
     4.9      Examples
    4.10  
    4.11  session SML in SML = Pure +
    4.12 -  options [condition = ISABELLE_POLYML]
    4.13 +  options [condition = ML_SYSTEM_POLYML]
    4.14    theories
    4.15      Examples
    4.16