# HG changeset patch
# User wenzelm
# Date 1348584932 -7200
# Node ID 4b2762e12b474fe1b07652e656e38d5d2af1f86b
# Parent  ba9dcdbf45f135f45bcb052eb267dd68999ad2eb
more complete build;
added option -c to imitate old browser;

diff -r ba9dcdbf45f1 -r 4b2762e12b47 src/Tools/Graphview/lib/Tools/graphview
--- a/src/Tools/Graphview/lib/Tools/graphview	Tue Sep 25 16:48:33 2012 +0200
+++ b/src/Tools/Graphview/lib/Tools/graphview	Tue Sep 25 16:55:32 2012 +0200
@@ -8,7 +8,6 @@
 ## sources
 
 declare -a SOURCES=(
-#  "src/dockable.scala"
   "src/floating_dialog.scala"
   "src/frame.scala"
   "src/graph_panel.scala"
@@ -39,6 +38,7 @@
   echo
   echo "  Options are:"
   echo "    -b           build only"
+  echo "    -c           cleanup -- remove GRAPH_FILE after use"
   echo "    -f           fresh build"
   echo
   exit 1
@@ -61,14 +61,18 @@
 # options
 
 BUILD_ONLY=false
+CLEAN=""
 BUILD_JARS="jars"
 
-while getopts "bf" OPT
+while getopts "bcf" OPT
 do
   case "$OPT" in
     b)
       BUILD_ONLY=true
       ;;
+    c)
+      CLEAN="true"
+      ;;
     f)
       BUILD_JARS="jars_fresh"
       ;;
@@ -78,6 +82,8 @@
   esac
 done
 
+shift $(($OPTIND - 1))
+
 
 # args
 
@@ -102,6 +108,7 @@
 
 PURE_JAR="$ISABELLE_HOME/lib/classes/ext/Pure.jar"
 COBRA_JAR="$ISABELLE_JEDIT_BUILD_HOME/contrib/cobra.jar"
+JS_JAR="$ISABELLE_JEDIT_BUILD_HOME/contrib/js.jar"
 
 TARGET_DIR="$ISABELLE_HOME/lib/classes"
 TARGET="$TARGET_DIR/ext/Graphview.jar"
@@ -116,7 +123,7 @@
     OUTDATED=true
   else
     if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
-      declare -a DEPS=("$COBRA_JAR" "$PURE_JAR" "${SOURCES[@]}")
+      declare -a DEPS=("$COBRA_JAR" "$JS_JAR" "$PURE_JAR" "${SOURCES[@]}")
     elif [ -e "$ISABELLE_HOME/Admin/build" ]; then
       declare -a DEPS=("$PURE_JAR" "${SOURCES[@]}")
     else
@@ -151,9 +158,10 @@
   rm -rf classes && mkdir classes
 
   cp -p -R -f "$COBRA_JAR" "$TARGET_DIR/ext" || failed
+  cp -p -R -f "$JS_JAR" "$TARGET_DIR/ext" || failed
 
   (
-    for JAR in "$COBRA_JAR" "$PURE_JAR"
+    for JAR in "$COBRA_JAR" "$JS_JAR" "$PURE_JAR"
     do
       CLASSPATH="$CLASSPATH:$JAR"
     done
@@ -172,6 +180,17 @@
 
 ## run
 
-[ "$BUILD_ONLY" = true ] || {
-  exec "$ISABELLE_TOOL" java isabelle.graphview.Graphview_Frame "$(jvmpath "$GRAPH_FILE")"
-}
+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 isabelle.graphview.Graphview_Frame "$(jvmpath "$PRIVATE_FILE")"
+  RC="$?"
+
+  rm -f "$PRIVATE_FILE"
+  echo "$RC"
+fi
diff -r ba9dcdbf45f1 -r 4b2762e12b47 src/Tools/Graphview/src/mutator.scala
--- a/src/Tools/Graphview/src/mutator.scala	Tue Sep 25 16:48:33 2012 +0200
+++ b/src/Tools/Graphview/src/mutator.scala	Tue Sep 25 16:55:32 2012 +0200
@@ -71,8 +71,7 @@
     name,
     description,
     g => (g /: g.dest) {
-      (graph, k) => {
-        val (from, tos) = k
+      case (graph, ((from, _), tos)) => {
         (graph /: tos) {
           (gr, to) => if (pred(gr, from, to)) gr
                       else gr.del_edge(from, to)