incorporate isabelle.graphview into Pure.jar, which saves 20..30s build time;
authorwenzelm
Wed, 21 May 2014 12:03:46 +0200
changeset 57032 cf570f3ecdc1
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
--- a/src/Pure/General/graph_display.ML	Wed May 21 10:13:12 2014 +0200
+++ b/src/Pure/General/graph_display.ML	Wed May 21 12:03:46 2014 +0200
@@ -59,9 +59,6 @@
   |> fold (fn {ID = a, parents = bs, ...} => fold (fn b => Graph.add_edge (b, a)) bs) graph
   |> let open XML.Encode in Graph.encode string (pair string encode_content) end;
 
-fun write_graph_graphview path graph =
-  File.write path (YXML.string_of_body (encode_graphview graph));
-
 
 (* display graph *)
 
@@ -76,14 +73,10 @@
     in writeln ("See " ^ bg1 ^ body ^ bg2 ^ "graph" ^ en) end
   else
     let
-      val (write, tool) =
-        if is_browser () then (write_graph_browser, "browser")
-        else (write_graph_graphview, "graphview");
-
       val _ = writeln "Displaying graph ...";
       val path = Isabelle_System.create_tmp_path "graph" "";
-      val _ = write path graph;
-      val _ = Isabelle_System.isabelle_tool tool ("-c " ^ File.shell_path path ^ " &");
+      val _ = write_graph_browser path graph;
+      val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
     in () end;
 
 end;
--- a/src/Pure/build-jars	Wed May 21 10:13:12 2014 +0200
+++ b/src/Pure/build-jars	Wed May 21 12:03:46 2014 +0200
@@ -97,6 +97,17 @@
   package.scala
   term.scala
   term_xml.scala
+  "../Tools/Graphview/src/graph_panel.scala"
+  "../Tools/Graphview/src/graphview.scala"
+  "../Tools/Graphview/src/layout_pendulum.scala"
+  "../Tools/Graphview/src/main_panel.scala"
+  "../Tools/Graphview/src/model.scala"
+  "../Tools/Graphview/src/mutator_dialog.scala"
+  "../Tools/Graphview/src/mutator_event.scala"
+  "../Tools/Graphview/src/mutator.scala"
+  "../Tools/Graphview/src/popups.scala"
+  "../Tools/Graphview/src/shapes.scala"
+  "../Tools/Graphview/src/visualizer.scala"
 )
 
 
--- a/src/Tools/Graphview/etc/settings	Wed May 21 10:13:12 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-GRAPHVIEW_HOME="$COMPONENT"
-
-GRAPHVIEW_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss4m"
-GRAPHVIEW_JAR="$ISABELLE_HOME/lib/classes/Graphview.jar"
-classpath "$GRAPHVIEW_JAR"
-
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$GRAPHVIEW_HOME/lib/Tools"
-
--- a/src/Tools/Graphview/lib/Tools/graphview	Wed May 21 10:13:12 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,175 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Kaiser, TU Muenchen
-# Author: Makarius
-#
-# DESCRIPTION: graphview command-line tool wrapper
-
-## sources
-
-declare -a SOURCES=(
-  "src/graph_panel.scala"
-  "src/graphview.scala"
-  "src/layout_pendulum.scala"
-  "src/main_panel.scala"
-  "src/model.scala"
-  "src/mutator_dialog.scala"
-  "src/mutator_event.scala"
-  "src/mutator.scala"
-  "src/popups.scala"
-  "src/shapes.scala"
-  "src/visualizer.scala"
-)
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: isabelle $PRG [OPTIONS] GRAPH_FILE"
-  echo
-  echo "  Options are:"
-  echo "    -b           build only"
-  echo "    -c           cleanup -- remove GRAPH_FILE after use"
-  echo "    -f           fresh build"
-  echo
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-function failed()
-{
-  fail "Failed!"
-}
-
-
-## process command line
-
-# options
-
-BUILD_ONLY="false"
-CLEAN="false"
-BUILD_JARS="jars"
-
-while getopts "bcf" OPT
-do
-  case "$OPT" in
-    b)
-      BUILD_ONLY="true"
-      ;;
-    c)
-      CLEAN="true"
-      ;;
-    f)
-      BUILD_JARS="jars_fresh"
-      ;;
-    \?)
-      usage
-      ;;
-  esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-GRAPH_FILE=""
-[ "$#" -gt 0 ] && { GRAPH_FILE="$1"; shift; }
-[ "$#" -ne 0 ] && usage
-[ -z "$GRAPH_FILE" -a "$BUILD_ONLY" = false ] && usage
-
-
-## build
-
-isabelle_admin_build "$BUILD_JARS" || exit $?
-
-pushd "$GRAPHVIEW_HOME" >/dev/null || failed
-
-PURE_JAR="$ISABELLE_HOME/lib/classes/Pure.jar"
-
-TARGET_DIR="$ISABELLE_HOME/lib/classes"
-TARGET="$TARGET_DIR/Graphview.jar"
-
-declare -a UPDATED=()
-
-if [ "$BUILD_JARS" = jars_fresh ]; then
-  OUTDATED=true
-else
-  OUTDATED=false
-  if [ ! -e "$TARGET" ]; then
-    OUTDATED=true
-  else
-    if [ -e "$ISABELLE_HOME/Admin/build" ]; then
-      declare -a DEPS=("$PURE_JAR" "${SOURCES[@]}")
-    else
-      declare -a DEPS=()
-    fi
-    for DEP in "${DEPS[@]}"
-    do
-      [ ! -e "$DEP" ] && fail "Missing file: $DEP"
-      [ "$DEP" -nt "$TARGET" ] && {
-        OUTDATED=true
-        UPDATED["${#UPDATED[@]}"]="$DEP"
-      }
-    done
-  fi
-fi
-
-if [ "$OUTDATED" = true ]
-then
-  echo "### Building Isabelle/Graphview ..."
-
-  [ "${#UPDATED[@]}" -gt 0 ] && {
-    echo "Changed files:"
-    for FILE in "${UPDATED[@]}"
-    do
-      echo "  $FILE"
-    done
-  }
-
-  rm -rf classes && mkdir classes
-
-  (
-    #FIXME workaround for scalac 2.11.0
-    function stty() { :; }
-    export -f stty
-
-    classpath "$PURE_JAR"
-    export CLASSPATH="$(jvmpath "$ISABELLE_CLASSPATH")"
-    exec "$SCALA_HOME/bin/scalac" $ISABELLE_SCALA_BUILD_OPTIONS -d classes "${SOURCES[@]}"
-  ) || fail "Failed to compile sources"
-
-  cd classes
-  isabelle_jdk jar cf "$(jvmpath "$TARGET")" * || failed
-  cd ..
-  rm -rf classes
-fi
-
-popd >/dev/null
-
-
-## run
-
-if [ "$BUILD_ONLY" = false ]; then
-  PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$""$(basename "$GRAPH_FILE")"
-  if [ "$CLEAN" = "true" ]; then
-    mv -f "$GRAPH_FILE" "$PRIVATE_FILE" || fail "Cannot move file: $GRAPH_FILE"
-  else
-    cp -f "$GRAPH_FILE" "$PRIVATE_FILE" || fail "Cannot copy file: $GRAPH_FILE"
-  fi
-
-  "$ISABELLE_TOOL" java $GRAPHVIEW_JAVA_OPTIONS isabelle.graphview.Graphview "$PRIVATE_FILE"
-  RC="$?"
-
-  rm -f "$PRIVATE_FILE"
-  echo "$RC"
-fi
--- a/src/Tools/jEdit/lib/Tools/jedit	Wed May 21 10:13:12 2014 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Wed May 21 12:03:46 2014 +0200
@@ -194,12 +194,7 @@
 
 if [ -e "$ISABELLE_HOME/Admin/build" ]; then
   "$ISABELLE_TOOL" browser -b || exit $?
-  if [ "$BUILD_JARS" = jars_fresh ]; then
-    "$ISABELLE_TOOL" graphview -b -f || exit $?
-  else
-    "$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?
-    "$ISABELLE_TOOL" graphview -b || exit $?
-  fi
+  "$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?
 fi
 
 PURE_JAR="$ISABELLE_HOME/lib/classes/Pure.jar"
@@ -238,11 +233,11 @@
   else
     if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
       declare -a DEPS=(
-        "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$GRAPHVIEW_JAR"
+        "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR"
         "${SOURCES[@]}" "${RESOURCES[@]}"
       )
     elif [ -e "$ISABELLE_HOME/Admin/build" ]; then
-      declare -a DEPS=("$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
+      declare -a DEPS=("$PURE_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
     else
       declare -a DEPS=()
     fi
@@ -316,7 +311,7 @@
     function stty() { :; }
     export -f stty
 
-    for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$GRAPHVIEW_JAR"
+    for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR"
     do
       classpath "$JAR"
     done