lib/Tools/console
changeset 62047 1ae53588dcbb
parent 61958 0a5dd617a88c
child 62509 13d6948e4b12
equal deleted inserted replaced
62046:2c9f68fbf047 62047:1ae53588dcbb
    42 
    42 
    43 ## process command line
    43 ## process command line
    44 
    44 
    45 # options
    45 # options
    46 
    46 
    47 declare -a ISABELLE_OPTIONS=(-m ASCII)
    47 declare -a ISABELLE_OPTIONS=()
    48 
    48 
    49 declare -a INCLUDE_DIRS=()
    49 declare -a INCLUDE_DIRS=()
    50 LOGIC="$ISABELLE_LOGIC"
    50 LOGIC="$ISABELLE_LOGIC"
    51 NO_BUILD="false"
    51 NO_BUILD="false"
    52 declare -a SYSTEM_OPTIONS=()
    52 declare -a SYSTEM_OPTIONS=()
   102   "${INCLUDE_DIRS[@]}" $'\n' "${SYSTEM_OPTIONS[@]}" || {
   102   "${INCLUDE_DIRS[@]}" $'\n' "${SYSTEM_OPTIONS[@]}" || {
   103   rm -f "$OPTIONS_FILE"
   103   rm -f "$OPTIONS_FILE"
   104   exit "$?"
   104   exit "$?"
   105 }
   105 }
   106 
   106 
       
   107 if [ "$LOGIC" != "RAW" ]; then
       
   108   ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-m"
       
   109   ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="ASCII"
       
   110 fi
       
   111 
   107 ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-O"
   112 ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="-O"
   108 ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTIONS_FILE"
   113 ISABELLE_OPTIONS["${#ISABELLE_OPTIONS[@]}"]="$OPTIONS_FILE"
   109 
   114 
   110 if type -p "$ISABELLE_LINE_EDITOR" > /dev/null
   115 if type -p "$ISABELLE_LINE_EDITOR" > /dev/null
   111 then
   116 then