# HG changeset patch # User wenzelm # Date 1356965777 -3600 # Node ID 5c85f8b80b95cc24048b6b3bfffaf39d99ec9ef4 # Parent ead5714cc4805954326c84df3090b9887a4d5a44 simplified quick start via "isabelle components -I"; diff -r ead5714cc480 -r 5c85f8b80b95 README_REPOSITORY --- a/README_REPOSITORY Mon Dec 31 14:58:21 2012 +0100 +++ b/README_REPOSITORY Mon Dec 31 15:56:17 2012 +0100 @@ -4,28 +4,25 @@ Quick start in 25min -------------------- -1a. Windows: ensure that Cygwin with Mercurial and Perl is installed; - see also http://www.cygwin.com/ - -1b. Mac OS X and Linux: ensure that Mercurial (hg) is installed; see +1a. Linux and Mac OS X: ensure that Mercurial (hg) is installed; see also http://www.selenic.com/mercurial -2. Create file $HOME/.isabelle/etc/settings and insert the following - line near its beginning: +1b. Windows: ensure that Cygwin with Mercurial and Perl is installed; + see also http://www.cygwin.com/ - init_components "$HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/main" - -3. Execute bash shell commands as follows: +2. Clone repository (bash shell commands): hg clone http://isabelle.in.tum.de/repos/isabelle cd isabelle + ./bin/isabelle components -I + ./bin/isabelle components -a ./bin/isabelle jedit -l HOL -4. To stay up-to-date later on, pull changes like this: +3. Update repository (bash shell commands): cd isabelle diff -r ead5714cc480 -r 5c85f8b80b95 lib/Tools/components --- a/lib/Tools/components Mon Dec 31 14:58:21 2012 +0100 +++ b/lib/Tools/components Mon Dec 31 15:56:17 2012 +0100 @@ -15,6 +15,7 @@ echo "Usage: isabelle $PRG [OPTIONS] [COMPONENTS ...]" echo echo " Options are:" + echo " -I init user settings" echo " -R URL component repository (default \$ISABELLE_COMPONENT_REPOSITORY)" echo " -a all missing components" echo " -l list status" @@ -38,13 +39,17 @@ #options +INIT_SETTINGS="" COMPONENT_REPOSITORY="$ISABELLE_COMPONENT_REPOSITORY" ALL_MISSING="" LIST_ONLY="" -while getopts "R:al" OPT +while getopts "IR:al" OPT do case "$OPT" in + I) + INIT_SETTINGS="true" + ;; R) COMPONENT_REPOSITORY="$OPTARG" ;; @@ -65,7 +70,7 @@ # args -[ "$#" -eq 0 -a -z "$ALL_MISSING" -a -z "$LIST_ONLY" ] && usage +[ "$#" -eq 0 -a -z "$INIT_SETTINGS" -a -z "$ALL_MISSING" -a -z "$LIST_ONLY" ] && usage if [ -z "$ALL_MISSING" ]; then splitarray ":" "$@" @@ -80,7 +85,23 @@ splitarray ":" "$ISABELLE_COMPONENTS"; declare -a AVAILABLE_COMPONENTS=("${SPLITARRAY[@]}") splitarray ":" "$ISABELLE_COMPONENTS_MISSING"; declare -a MISSING_COMPONENTS=("${SPLITARRAY[@]}") -if [ -n "$LIST_ONLY" ]; then +if [ -n "$INIT_SETTINGS" ]; then + SETTINGS="$ISABELLE_HOME_USER/etc/settings" + SETTINGS_CONTENT='init_components "$USER_HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/main"' + if [ -e "$SETTINGS" ]; then + echo "User settings file already exists!" + echo + echo "Edit \"$SETTINGS\" manually" + echo "and add the following line near its start:" + echo + echo " $SETTINGS_CONTENT" + echo + else + echo "Initializing \"$SETTINGS\"" + mkdir -p "$(dirname "$SETTINGS")" + echo "$SETTINGS_CONTENT" > "$SETTINGS" + fi +elif [ -n "$LIST_ONLY" ]; then echo echo "Available components:" for NAME in "${AVAILABLE_COMPONENTS[@]}"; do echo " $NAME"; done diff -r ead5714cc480 -r 5c85f8b80b95 src/Doc/System/Misc.thy --- a/src/Doc/System/Misc.thy Mon Dec 31 14:58:21 2012 +0100 +++ b/src/Doc/System/Misc.thy Mon Dec 31 15:56:17 2012 +0100 @@ -18,6 +18,7 @@ Usage: isabelle components [OPTIONS] [COMPONENTS ...] Options are: + -I init user settings -R URL component repository (default $ISABELLE_COMPONENT_REPOSITORY) -a all missing components @@ -49,7 +50,14 @@ Option @{verbatim "-l"} lists the current state of available and missing components with their location (full name) within the - file-system. *} + file-system. + + Option @{verbatim "-I"} initializes the user settings file to + subscribe to the standard components specified in the Isabelle + repository clone --- this does not make any sense for regular + Isabelle releases. If the file already exists, it needs to be + edited manually according to the printed explanation. +*} section {* Displaying documents *}