Gedichte Musik Bilder Quellcodebibliothek Diashow Normaldarstellung
products/sources/formale sprachen/Isabelle/Tools/jEdit/lib/Tools/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: jedit   Sprache: Python

Original von: Isabelle©
#!/usr/bin/env bash
#
# Author: Makarius
#
# DESCRIPTION: Isabelle/jEdit interface wrapper


## sources

declare -a SOURCES0=(
  "src/Tools/jEdit/src-base/dockable.scala"
  "src/Tools/jEdit/src-base/isabelle_encoding.scala"
  "src/Tools/jEdit/src-base/jedit_lib.scala"
  "src/Tools/jEdit/src-base/pide_docking_framework.scala"
  "src/Tools/jEdit/src-base/plugin.scala"
  "src/Tools/jEdit/src-base/syntax_style.scala"
)

declare -a RESOURCES0=(
  "src/Tools/jEdit/src-base/Isabelle_Base.props"
  "src/Tools/jEdit/src-base/services.xml"
)

declare -a SOURCES=(
  "src/Tools/jEdit/src/active.scala"
  "src/Tools/jEdit/src/completion_popup.scala"
  "src/Tools/jEdit/src/context_menu.scala"
  "src/Tools/jEdit/src/debugger_dockable.scala"
  "src/Tools/jEdit/src/document_model.scala"
  "src/Tools/jEdit/src/document_view.scala"
  "src/Tools/jEdit/src/documentation_dockable.scala"
  "src/Tools/jEdit/src/fold_handling.scala"
  "src/Tools/jEdit/src/font_info.scala"
  "src/Tools/jEdit/src/graphview_dockable.scala"
  "src/Tools/jEdit/src/info_dockable.scala"
  "src/Tools/jEdit/src/isabelle.scala"
  "src/Tools/jEdit/src/isabelle_encoding.scala"
  "src/Tools/jEdit/src/isabelle_export.scala"
  "src/Tools/jEdit/src/isabelle_options.scala"
  "src/Tools/jEdit/src/isabelle_session.scala"
  "src/Tools/jEdit/src/isabelle_sidekick.scala"
  "src/Tools/jEdit/src/isabelle_vfs.scala"
  "src/Tools/jEdit/src/jedit_bibtex.scala"
  "src/Tools/jEdit/src/jedit_editor.scala"
  "src/Tools/jEdit/src/jedit_lib.scala"
  "src/Tools/jEdit/src/jedit_options.scala"
  "src/Tools/jEdit/src/jedit_rendering.scala"
  "src/Tools/jEdit/src/jedit_resources.scala"
  "src/Tools/jEdit/src/jedit_sessions.scala"
  "src/Tools/jEdit/src/jedit_spell_checker.scala"
  "src/Tools/jEdit/src/keymap_merge.scala"
  "src/Tools/jEdit/src/monitor_dockable.scala"
  "src/Tools/jEdit/src/output_dockable.scala"
  "src/Tools/jEdit/src/plugin.scala"
  "src/Tools/jEdit/src/pretty_text_area.scala"
  "src/Tools/jEdit/src/pretty_tooltip.scala"
  "src/Tools/jEdit/src/process_indicator.scala"
  "src/Tools/jEdit/src/protocol_dockable.scala"
  "src/Tools/jEdit/src/query_dockable.scala"
  "src/Tools/jEdit/src/raw_output_dockable.scala"
  "src/Tools/jEdit/src/rich_text_area.scala"
  "src/Tools/jEdit/src/scala_console.scala"
  "src/Tools/jEdit/src/session_build.scala"
  "src/Tools/jEdit/src/simplifier_trace_dockable.scala"
  "src/Tools/jEdit/src/simplifier_trace_window.scala"
  "src/Tools/jEdit/src/sledgehammer_dockable.scala"
  "src/Tools/jEdit/src/state_dockable.scala"
  "src/Tools/jEdit/src/status_widget.scala"
  "src/Tools/jEdit/src/symbols_dockable.scala"
  "src/Tools/jEdit/src/syntax_style.scala"
  "src/Tools/jEdit/src/syslog_dockable.scala"
  "src/Tools/jEdit/src/text_overview.scala"
  "src/Tools/jEdit/src/text_structure.scala"
  "src/Tools/jEdit/src/theories_dockable.scala"
  "src/Tools/jEdit/src/timing_dockable.scala"
  "src/Tools/jEdit/src/token_markup.scala"
)

declare -a RESOURCES=(
  "src/Tools/jEdit/src/actions.xml"
  "src/Tools/jEdit/src/dockables.xml"
  "src/Tools/jEdit/src/Isabelle.props"
  "src/Tools/jEdit/src/jEdit.props"
  "src/Tools/jEdit/src/services.xml"
  "src/Tools/jEdit/src/modes/isabelle-ml.xml"
  "src/Tools/jEdit/src/modes/isabelle-news.xml"
  "src/Tools/jEdit/src/modes/isabelle-options.xml"
  "src/Tools/jEdit/src/modes/isabelle-root.xml"
  "src/Tools/jEdit/src/modes/isabelle.xml"
  "src/Tools/jEdit/src/modes/sml.xml"
)


## diagnostics

PRG="$(basename "$0")"

function usage()
{
  echo
  echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
  echo
  echo "  Options are:"
  echo "    -A NAME      ancestor session for option -R (default: parent)"
  echo "    -D NAME=X    set JVM system property"
  echo "    -J OPTION    add JVM runtime option"
  echo "                 (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
  echo "    -R NAME      build image with requirements from other sessions"
  echo "    -b           build only"
  echo "    -d DIR       include session directory"
  echo "    -f           fresh build"
  echo "    -i NAME      include session in name-space of theories"
  echo "    -j OPTION    add jEdit runtime option"
  echo "                 (default $JEDIT_OPTIONS)"
  echo "    -l NAME      logic session name"
  echo "    -m MODE      add print mode for output"
  echo "    -n           no build of session image on startup"
  echo "    -p CMD       ML process command prefix (process policy)"
  echo "    -s           system build mode for session image (system_heaps=true)"
  echo "    -u           user build mode for session image (system_heaps=false)"
  echo
  echo "  Start jEdit with Isabelle plugin setup and open FILES"
  echo "  (default \"$USER_HOME/Scratch.thy\" or \":\" for empty buffer)."
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}

function failed()
{
  fail "Failed!"
}


## process command line

# options

BUILD_ONLY=false
FRESH_BUILD=""
ML_PROCESS_POLICY=""
JEDIT_LOGIC_ANCESTOR=""
JEDIT_LOGIC_REQUIREMENTS=""
JEDIT_INCLUDE_SESSIONS=""
JEDIT_SESSION_DIRS="-"
JEDIT_LOGIC=""
JEDIT_PRINT_MODE=""
JEDIT_NO_BUILD=""
JEDIT_BUILD_MODE="default"

function getoptions()
{
  OPTIND=1
  while getopts "A:BFD:J:R:bd:fi:j:l:m:np:su" OPT
  do
    case "$OPT" in
      A)
        JEDIT_LOGIC_ANCESTOR="$OPTARG"
        ;;
      D)
        JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG"
        ;;
      J)
        JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
        ;;
      R)
        JEDIT_LOGIC="$OPTARG"
        JEDIT_LOGIC_REQUIREMENTS="true"
        ;;
      b)
        BUILD_ONLY=true
        ;;
      d)
        JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG"
        ;;
      i)
        if [ -z "$JEDIT_INCLUDE_SESSIONS" ]; then
          JEDIT_INCLUDE_SESSIONS="$OPTARG"
        else
          JEDIT_INCLUDE_SESSIONS="$JEDIT_INCLUDE_SESSIONS:$OPTARG"
        fi
        ;;
      f)
        FRESH_BUILD="true"
        ;;
      j)
        ARGS["${#ARGS[@]}"]="$OPTARG"
        ;;
      l)
        JEDIT_LOGIC="$OPTARG"
        ;;
      m)
        if [ -z "$JEDIT_PRINT_MODE" ]; then
          JEDIT_PRINT_MODE="$OPTARG"
        else
          JEDIT_PRINT_MODE="$JEDIT_PRINT_MODE,$OPTARG"
        fi
        ;;
      n)
        JEDIT_NO_BUILD="true"
        ;;
      p)
        ML_PROCESS_POLICY="$OPTARG"
        ;;
      s)
        JEDIT_BUILD_MODE="system"
        ;;
      u)
        JEDIT_BUILD_MODE="user"
        ;;
      \?)
        usage
        ;;
    esac
  done
}

eval "declare -a JAVA_ARGS=($JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"

declare -a ARGS=()

declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)"
getoptions "${OPTIONS[@]}"

getoptions "$@"
shift $(($OPTIND - 1))


# args

while [ "$#" -gt 0 ]; do
  ARGS["${#ARGS[@]}"]="$(platform_path "$1")"
  shift
done


## dependencies

if [ -e "$ISABELLE_HOME/Admin/build" ]; then
  isabelle browser -b || exit $?
  if [ -n "$FRESH_BUILD" ]; then
    "$ISABELLE_HOME/Admin/build" jars_fresh || exit $?
  else
    "$ISABELLE_HOME/Admin/build" jars || exit $?
  fi
elif [ -n "$FRESH_BUILD" ]; then
  echo >&2 "### Ignoring fresh build option: not a repository clone"
  FRESH_BUILD=""
fi

JEDIT_BUILD_JAR="$ISABELLE_JEDIT_BUILD_VERSION/jedit.jar"

declare -a JEDIT_BUILD_JARS=(
  "Code2HTML.jar"
  "CommonControls.jar"
  "Console.jar"
  "ErrorList.jar"
  "Highlight.jar"
  "kappalayout.jar"
  "Navigator.jar"
  "SideKick.jar"
  "idea-icons.jar"
  "jsr305-2.0.0.jar"
)


# target

pushd "$ISABELLE_HOME" >/dev/null || failed

TARGET_DIR="src/Tools/jEdit/dist"
TARGET_JAR0="$TARGET_DIR/jars/Isabelle-jEdit-base.jar"
TARGET_JAR="$TARGET_DIR/jars/Isabelle-jEdit.jar"
TARGET_SHASUM="$TARGET_DIR/Isabelle-jEdit.shasum"

declare -a TARGET_DEPS=("lib/classes/Pure.jar" "$TARGET_DIR/jedit.jar")
for DEP in "${JEDIT_BUILD_JARS[@]}"
do
  TARGET_DEPS["${#TARGET_DEPS[@]}"]="$TARGET_DIR/jars/$DEP"
done

function target_shasum()
(
  shasum -a1 -b "$TARGET_JAR0" "$TARGET_JAR" "${TARGET_DEPS[@]}" \
    "${SOURCES0[@]}" "${RESOURCES0[@]}" "${SOURCES[@]}" "${RESOURCES[@]}" 2>/dev/null
)

function target_clean()
{
  rm -rf "$ISABELLE_HOME/$TARGET_DIR"
}

[ -n "$FRESH_BUILD" ] && target_clean


## build

BUILD_DIR="$TARGET_DIR/build"

function init_resources ()
{
  mkdir -p "$BUILD_DIR" || failed
  cp -p -R "$@" "$BUILD_DIR/."
}

function compile_sources()
{
  (
    #FIXME workarounds for scalac 2.11.0
    export CYGWIN="nodosfilewarning"
    function stty() { :; }
    export -f stty

    for DEP in "${TARGET_DEPS[@]}"
    do
      classpath "$DEP"
    done
    export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")"
    isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d "$BUILD_DIR" "$@"
  ) || fail "Failed to compile sources"
}

function make_jar()
{
  isabelle_jdk jar -c -f "$1" -C "$BUILD_DIR" . || failed
  rm -rf "$ISABELLE_HOME/$BUILD_DIR"
}

target_shasum | cmp "$TARGET_SHASUM" >/dev/null 2>/dev/null
if [ -e "$ISABELLE_HOME/Admin/build" -a "$?" -ne 0 ]; then
  echo "### Building Isabelle/jEdit ..."

  [ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \
    fail "Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component"

  target_clean || failed
  mkdir -p "$TARGET_DIR" || failed

  cp -p -R "$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/." "$TARGET_DIR/."

  for DEP in "${JEDIT_BUILD_JARS[@]}"
  do
    cp -p "$ISABELLE_JEDIT_BUILD_HOME/contrib/$DEP" "$TARGET_DIR/jars/."
  done

  init_resources "${RESOURCES0[@]}"
  compile_sources "${SOURCES0[@]}"
  make_jar "$TARGET_JAR0"
  classpath "$TARGET_JAR0"

  init_resources "${RESOURCES[@]}"
  cp src/Tools/jEdit/src/jEdit.props "$TARGET_DIR/properties/."
  cp -p -R -f "src/Tools/jEdit/src/modes/." "$TARGET_DIR/modes/."

  perl -i -e 'while (<>) {
    if (m/FILE="ml.xml"/ or m/FILE_NAME_GLOB="...sml,ml."/ or m/FILE_NAME_GLOB="..ftl"/) { }
    elsif (m/NAME="javacc"/) {
      print qq!<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="{*.thy,ROOT0.ML,ROOT.ML}"/>\n\n!;
      print qq!<MODE NAME="isabelle-ml" FILE="isabelle-ml.xml" FILE_NAME_GLOB="*.ML"/>\n\n!;
      print qq!<MODE NAME="isabelle-news" FILE="isabelle-news.xml"/>\n\n!;
      print qq!<MODE NAME="isabelle-options" FILE="isabelle-options.xml"/>\n\n!;
      print qq!<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>\n\n!;
      print;
    }
    elsif (m/NAME="sqr"/) {
      print qq!<MODE NAME="sml" FILE="sml.xml" FILE_NAME_GLOB="*.{sml,sig}"/>\n\n!;
      print;
    }
    else { print; }
  }' "$TARGET_DIR/modes/catalog"

  (
    cd "$TARGET_DIR"
    isabelle_jdk jar -x -f jedit.jar
    cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" \
      "org/gjt/sp/jedit/icons/themes/classic/32x32/apps/isabelle.gif" || failed
    cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" \
      "org/gjt/sp/jedit/icons/themes/tango/32x32/apps/isabelle.gif" || failed
    isabelle_jdk jar -c -f jedit.jar -e org.gjt.sp.jedit.jEdit org || failed
    rm -rf META-INF org
  )

  compile_sources "${SOURCES[@]}"
  make_jar "$TARGET_JAR"

  target_shasum > "$TARGET_SHASUM"

  cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.6.0manual-a4.pdf" "$TARGET_DIR/doc/jedit-manual.pdf"
  cp "$TARGET_DIR/doc/CHANGES.txt" "$TARGET_DIR/doc/jedit-changes"
  cat > "$TARGET_DIR/doc/Contents" <<EOF
Original jEdit Documentation
  jedit-manual    jEdit 5.6 User's Guide
  jedit-changes   jEdit 5.6 Version History

EOF

fi


## main

popd >/dev/null

if [ "$BUILD_ONLY" = false ]
then
  "$ISABELLE_HOME/lib/scripts/java-gui-setup"

  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \
    JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_NO_BUILD JEDIT_BUILD_MODE
  export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
  classpath "$JEDIT_HOME/dist/jedit.jar"
  exec isabelle java -splash:"$(platform_path "$ISABELLE_HOME/lib/logo/isabelle.gif")" \
    "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
fi

¤ Dauer der Verarbeitung: 0.17 Sekunden  (vorverarbeitet)  ¤



Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff