incorporate isabelle.graphview into Pure.jar, which saves 20..30s build time;
authorwenzelm
Wed May 21 12:03:46 2014 +0200 (2014-05-21)
changeset 57032cf570f3ecdc1
parent 57031 30ee1453a954
child 57033 b24e2b83917f
incorporate isabelle.graphview into Pure.jar, which saves 20..30s build time;
discontinued pointless "isabelle graphview" command-line tool (Proof General legacy);
src/Pure/General/graph_display.ML
src/Pure/build-jars
src/Tools/Graphview/etc/settings
src/Tools/Graphview/lib/Tools/graphview
src/Tools/jEdit/lib/Tools/jedit
     1.1 --- a/src/Pure/General/graph_display.ML	Wed May 21 10:13:12 2014 +0200
     1.2 +++ b/src/Pure/General/graph_display.ML	Wed May 21 12:03:46 2014 +0200
     1.3 @@ -59,9 +59,6 @@
     1.4    |> fold (fn {ID = a, parents = bs, ...} => fold (fn b => Graph.add_edge (b, a)) bs) graph
     1.5    |> let open XML.Encode in Graph.encode string (pair string encode_content) end;
     1.6  
     1.7 -fun write_graph_graphview path graph =
     1.8 -  File.write path (YXML.string_of_body (encode_graphview graph));
     1.9 -
    1.10  
    1.11  (* display graph *)
    1.12  
    1.13 @@ -76,14 +73,10 @@
    1.14      in writeln ("See " ^ bg1 ^ body ^ bg2 ^ "graph" ^ en) end
    1.15    else
    1.16      let
    1.17 -      val (write, tool) =
    1.18 -        if is_browser () then (write_graph_browser, "browser")
    1.19 -        else (write_graph_graphview, "graphview");
    1.20 -
    1.21        val _ = writeln "Displaying graph ...";
    1.22        val path = Isabelle_System.create_tmp_path "graph" "";
    1.23 -      val _ = write path graph;
    1.24 -      val _ = Isabelle_System.isabelle_tool tool ("-c " ^ File.shell_path path ^ " &");
    1.25 +      val _ = write_graph_browser path graph;
    1.26 +      val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
    1.27      in () end;
    1.28  
    1.29  end;
     2.1 --- a/src/Pure/build-jars	Wed May 21 10:13:12 2014 +0200
     2.2 +++ b/src/Pure/build-jars	Wed May 21 12:03:46 2014 +0200
     2.3 @@ -97,6 +97,17 @@
     2.4    package.scala
     2.5    term.scala
     2.6    term_xml.scala
     2.7 +  "../Tools/Graphview/src/graph_panel.scala"
     2.8 +  "../Tools/Graphview/src/graphview.scala"
     2.9 +  "../Tools/Graphview/src/layout_pendulum.scala"
    2.10 +  "../Tools/Graphview/src/main_panel.scala"
    2.11 +  "../Tools/Graphview/src/model.scala"
    2.12 +  "../Tools/Graphview/src/mutator_dialog.scala"
    2.13 +  "../Tools/Graphview/src/mutator_event.scala"
    2.14 +  "../Tools/Graphview/src/mutator.scala"
    2.15 +  "../Tools/Graphview/src/popups.scala"
    2.16 +  "../Tools/Graphview/src/shapes.scala"
    2.17 +  "../Tools/Graphview/src/visualizer.scala"
    2.18  )
    2.19  
    2.20  
     3.1 --- a/src/Tools/Graphview/etc/settings	Wed May 21 10:13:12 2014 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,10 +0,0 @@
     3.4 -# -*- shell-script -*- :mode=shellscript:
     3.5 -
     3.6 -GRAPHVIEW_HOME="$COMPONENT"
     3.7 -
     3.8 -GRAPHVIEW_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss4m"
     3.9 -GRAPHVIEW_JAR="$ISABELLE_HOME/lib/classes/Graphview.jar"
    3.10 -classpath "$GRAPHVIEW_JAR"
    3.11 -
    3.12 -ISABELLE_TOOLS="$ISABELLE_TOOLS:$GRAPHVIEW_HOME/lib/Tools"
    3.13 -
     4.1 --- a/src/Tools/Graphview/lib/Tools/graphview	Wed May 21 10:13:12 2014 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,175 +0,0 @@
     4.4 -#!/usr/bin/env bash
     4.5 -#
     4.6 -# Author: Markus Kaiser, TU Muenchen
     4.7 -# Author: Makarius
     4.8 -#
     4.9 -# DESCRIPTION: graphview command-line tool wrapper
    4.10 -
    4.11 -## sources
    4.12 -
    4.13 -declare -a SOURCES=(
    4.14 -  "src/graph_panel.scala"
    4.15 -  "src/graphview.scala"
    4.16 -  "src/layout_pendulum.scala"
    4.17 -  "src/main_panel.scala"
    4.18 -  "src/model.scala"
    4.19 -  "src/mutator_dialog.scala"
    4.20 -  "src/mutator_event.scala"
    4.21 -  "src/mutator.scala"
    4.22 -  "src/popups.scala"
    4.23 -  "src/shapes.scala"
    4.24 -  "src/visualizer.scala"
    4.25 -)
    4.26 -
    4.27 -
    4.28 -## diagnostics
    4.29 -
    4.30 -PRG="$(basename "$0")"
    4.31 -
    4.32 -function usage()
    4.33 -{
    4.34 -  echo
    4.35 -  echo "Usage: isabelle $PRG [OPTIONS] GRAPH_FILE"
    4.36 -  echo
    4.37 -  echo "  Options are:"
    4.38 -  echo "    -b           build only"
    4.39 -  echo "    -c           cleanup -- remove GRAPH_FILE after use"
    4.40 -  echo "    -f           fresh build"
    4.41 -  echo
    4.42 -  exit 1
    4.43 -}
    4.44 -
    4.45 -function fail()
    4.46 -{
    4.47 -  echo "$1" >&2
    4.48 -  exit 2
    4.49 -}
    4.50 -
    4.51 -function failed()
    4.52 -{
    4.53 -  fail "Failed!"
    4.54 -}
    4.55 -
    4.56 -
    4.57 -## process command line
    4.58 -
    4.59 -# options
    4.60 -
    4.61 -BUILD_ONLY="false"
    4.62 -CLEAN="false"
    4.63 -BUILD_JARS="jars"
    4.64 -
    4.65 -while getopts "bcf" OPT
    4.66 -do
    4.67 -  case "$OPT" in
    4.68 -    b)
    4.69 -      BUILD_ONLY="true"
    4.70 -      ;;
    4.71 -    c)
    4.72 -      CLEAN="true"
    4.73 -      ;;
    4.74 -    f)
    4.75 -      BUILD_JARS="jars_fresh"
    4.76 -      ;;
    4.77 -    \?)
    4.78 -      usage
    4.79 -      ;;
    4.80 -  esac
    4.81 -done
    4.82 -
    4.83 -shift $(($OPTIND - 1))
    4.84 -
    4.85 -
    4.86 -# args
    4.87 -
    4.88 -GRAPH_FILE=""
    4.89 -[ "$#" -gt 0 ] && { GRAPH_FILE="$1"; shift; }
    4.90 -[ "$#" -ne 0 ] && usage
    4.91 -[ -z "$GRAPH_FILE" -a "$BUILD_ONLY" = false ] && usage
    4.92 -
    4.93 -
    4.94 -## build
    4.95 -
    4.96 -isabelle_admin_build "$BUILD_JARS" || exit $?
    4.97 -
    4.98 -pushd "$GRAPHVIEW_HOME" >/dev/null || failed
    4.99 -
   4.100 -PURE_JAR="$ISABELLE_HOME/lib/classes/Pure.jar"
   4.101 -
   4.102 -TARGET_DIR="$ISABELLE_HOME/lib/classes"
   4.103 -TARGET="$TARGET_DIR/Graphview.jar"
   4.104 -
   4.105 -declare -a UPDATED=()
   4.106 -
   4.107 -if [ "$BUILD_JARS" = jars_fresh ]; then
   4.108 -  OUTDATED=true
   4.109 -else
   4.110 -  OUTDATED=false
   4.111 -  if [ ! -e "$TARGET" ]; then
   4.112 -    OUTDATED=true
   4.113 -  else
   4.114 -    if [ -e "$ISABELLE_HOME/Admin/build" ]; then
   4.115 -      declare -a DEPS=("$PURE_JAR" "${SOURCES[@]}")
   4.116 -    else
   4.117 -      declare -a DEPS=()
   4.118 -    fi
   4.119 -    for DEP in "${DEPS[@]}"
   4.120 -    do
   4.121 -      [ ! -e "$DEP" ] && fail "Missing file: $DEP"
   4.122 -      [ "$DEP" -nt "$TARGET" ] && {
   4.123 -        OUTDATED=true
   4.124 -        UPDATED["${#UPDATED[@]}"]="$DEP"
   4.125 -      }
   4.126 -    done
   4.127 -  fi
   4.128 -fi
   4.129 -
   4.130 -if [ "$OUTDATED" = true ]
   4.131 -then
   4.132 -  echo "### Building Isabelle/Graphview ..."
   4.133 -
   4.134 -  [ "${#UPDATED[@]}" -gt 0 ] && {
   4.135 -    echo "Changed files:"
   4.136 -    for FILE in "${UPDATED[@]}"
   4.137 -    do
   4.138 -      echo "  $FILE"
   4.139 -    done
   4.140 -  }
   4.141 -
   4.142 -  rm -rf classes && mkdir classes
   4.143 -
   4.144 -  (
   4.145 -    #FIXME workaround for scalac 2.11.0
   4.146 -    function stty() { :; }
   4.147 -    export -f stty
   4.148 -
   4.149 -    classpath "$PURE_JAR"
   4.150 -    export CLASSPATH="$(jvmpath "$ISABELLE_CLASSPATH")"
   4.151 -    exec "$SCALA_HOME/bin/scalac" $ISABELLE_SCALA_BUILD_OPTIONS -d classes "${SOURCES[@]}"
   4.152 -  ) || fail "Failed to compile sources"
   4.153 -
   4.154 -  cd classes
   4.155 -  isabelle_jdk jar cf "$(jvmpath "$TARGET")" * || failed
   4.156 -  cd ..
   4.157 -  rm -rf classes
   4.158 -fi
   4.159 -
   4.160 -popd >/dev/null
   4.161 -
   4.162 -
   4.163 -## run
   4.164 -
   4.165 -if [ "$BUILD_ONLY" = false ]; then
   4.166 -  PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$""$(basename "$GRAPH_FILE")"
   4.167 -  if [ "$CLEAN" = "true" ]; then
   4.168 -    mv -f "$GRAPH_FILE" "$PRIVATE_FILE" || fail "Cannot move file: $GRAPH_FILE"
   4.169 -  else
   4.170 -    cp -f "$GRAPH_FILE" "$PRIVATE_FILE" || fail "Cannot copy file: $GRAPH_FILE"
   4.171 -  fi
   4.172 -
   4.173 -  "$ISABELLE_TOOL" java $GRAPHVIEW_JAVA_OPTIONS isabelle.graphview.Graphview "$PRIVATE_FILE"
   4.174 -  RC="$?"
   4.175 -
   4.176 -  rm -f "$PRIVATE_FILE"
   4.177 -  echo "$RC"
   4.178 -fi
     5.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Wed May 21 10:13:12 2014 +0200
     5.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Wed May 21 12:03:46 2014 +0200
     5.3 @@ -194,12 +194,7 @@
     5.4  
     5.5  if [ -e "$ISABELLE_HOME/Admin/build" ]; then
     5.6    "$ISABELLE_TOOL" browser -b || exit $?
     5.7 -  if [ "$BUILD_JARS" = jars_fresh ]; then
     5.8 -    "$ISABELLE_TOOL" graphview -b -f || exit $?
     5.9 -  else
    5.10 -    "$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?
    5.11 -    "$ISABELLE_TOOL" graphview -b || exit $?
    5.12 -  fi
    5.13 +  "$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?
    5.14  fi
    5.15  
    5.16  PURE_JAR="$ISABELLE_HOME/lib/classes/Pure.jar"
    5.17 @@ -238,11 +233,11 @@
    5.18    else
    5.19      if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
    5.20        declare -a DEPS=(
    5.21 -        "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$GRAPHVIEW_JAR"
    5.22 +        "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR"
    5.23          "${SOURCES[@]}" "${RESOURCES[@]}"
    5.24        )
    5.25      elif [ -e "$ISABELLE_HOME/Admin/build" ]; then
    5.26 -      declare -a DEPS=("$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
    5.27 +      declare -a DEPS=("$PURE_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
    5.28      else
    5.29        declare -a DEPS=()
    5.30      fi
    5.31 @@ -316,7 +311,7 @@
    5.32      function stty() { :; }
    5.33      export -f stty
    5.34  
    5.35 -    for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$GRAPHVIEW_JAR"
    5.36 +    for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR"
    5.37      do
    5.38        classpath "$JAR"
    5.39      done