merged
authorwenzelm
Mon Sep 19 22:48:05 2011 +0200 (2011-09-19)
changeset 450045bd261075711
parent 45003 7591039fb6b4
parent 44993 9a2d100dd3eb
child 45005 0d2d59525912
merged
     1.1 --- a/Admin/MacOS/App1/script	Mon Sep 19 16:18:34 2011 +0200
     1.2 +++ b/Admin/MacOS/App1/script	Mon Sep 19 22:48:05 2011 +0200
     1.3 @@ -12,7 +12,9 @@
     1.4  # sane environment defaults
     1.5  
     1.6  cd "$HOME"
     1.7 -PATH="$PATH:/opt/local/bin"
     1.8 +if [ -x /usr/libexec/path_helper ]; then
     1.9 +  eval $(/usr/libexec/path_helper -s)
    1.10 +fi
    1.11  
    1.12  [ -z "$LANG" ] && export LANG=en_US.UTF-8
    1.13  
     2.1 --- a/Admin/isatest/isatest-stats	Mon Sep 19 16:18:34 2011 +0200
     2.2 +++ b/Admin/isatest/isatest-stats	Mon Sep 19 22:48:05 2011 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  
     2.5  THIS="$(cd "$(dirname "$0")"; pwd)"
     2.6  
     2.7 -PLATFORMS="at-poly at-poly-test afp at64-poly cygwin-poly-e mac-poly-M2 mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at64-poly-5.1-para at-mac-poly-5.1-para at-sml-dev"
     2.8 +PLATFORMS="at-poly at-poly-test afp at64-poly cygwin-poly-e mac-poly-M2 mac-poly-M4 mac-poly64-M2 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at64-poly-5.1-para at-mac-poly-5.1-para at-sml-dev"
     2.9  
    2.10  ISABELLE_SESSIONS="\
    2.11    HOL-Plain \
     3.1 --- a/lib/Tools/display	Mon Sep 19 16:18:34 2011 +0200
     3.2 +++ b/lib/Tools/display	Mon Sep 19 22:48:05 2011 +0200
     3.3 @@ -74,7 +74,6 @@
     3.4    PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$FILE")
     3.5    mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
     3.6    $VIEWER "$PRIVATE_FILE"
     3.7 -  sleep 5   #try to avoid races
     3.8    rm -f "$PRIVATE_FILE"
     3.9  else
    3.10    exec $VIEWER "$FILE"
     4.1 --- a/src/Pure/General/symbol.scala	Mon Sep 19 16:18:34 2011 +0200
     4.2 +++ b/src/Pure/General/symbol.scala	Mon Sep 19 22:48:05 2011 +0200
     4.3 @@ -352,6 +352,8 @@
     4.4      val sym_chars =
     4.5        Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
     4.6  
     4.7 +    val symbolic = recode_set((for { (sym, _) <- symbols; if raw_symbolic(sym) } yield sym): _*)
     4.8 +
     4.9  
    4.10      /* control symbols */
    4.11  
    4.12 @@ -391,11 +393,16 @@
    4.13    def is_quasi(sym: Symbol): Boolean = sym == "_" || sym == "'"
    4.14    def is_letdig(sym: Symbol): Boolean = is_letter(sym) || is_digit(sym) || is_quasi(sym)
    4.15    def is_blank(sym: Symbol): Boolean = symbols.blanks.contains(sym)
    4.16 +
    4.17    def is_symbolic_char(sym: Symbol): Boolean = symbols.sym_chars.contains(sym)
    4.18 -  def is_symbolic(sym: Symbol): Boolean =
    4.19 +  def is_symbolic(sym: Symbol): Boolean = raw_symbolic(sym) || symbols.symbolic.contains(sym)
    4.20 +
    4.21 +  private def raw_symbolic(sym: Symbol): Boolean =
    4.22      sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
    4.23  
    4.24  
    4.25 +
    4.26 +
    4.27    /* control symbols */
    4.28  
    4.29    def is_ctrl(sym: Symbol): Boolean =
     5.1 --- a/src/Pure/System/isabelle_process.ML	Mon Sep 19 16:18:34 2011 +0200
     5.2 +++ b/src/Pure/System/isabelle_process.ML	Mon Sep 19 22:48:05 2011 +0200
     5.3 @@ -177,6 +177,9 @@
     5.4  
     5.5      val _ = quick_and_dirty := true;
     5.6      val _ = Goal.parallel_proofs := 0;
     5.7 +    val _ =
     5.8 +      if Multithreading.max_threads_value () < 2
     5.9 +      then Multithreading.max_threads := 2 else ();
    5.10      val _ = Context.set_thread_data NONE;
    5.11      val _ =
    5.12        Unsynchronized.change print_mode
     6.1 --- a/src/Pure/Thy/present.ML	Mon Sep 19 16:18:34 2011 +0200
     6.2 +++ b/src/Pure/Thy/present.ML	Mon Sep 19 22:48:05 2011 +0200
     6.3 @@ -499,8 +499,8 @@
     6.4          val base = Path.base path;
     6.5          val name =
     6.6            (case Path.implode (#1 (Path.split_ext base)) of
     6.7 -            "" => "DUMMY" ^ serial_string ()
     6.8 -          | s => s);
     6.9 +            "" => "DUMMY"
    6.10 +          | s => s)  ^ serial_string ();
    6.11        in
    6.12          if File.exists path then
    6.13            (((name, base, File.read path), (i, Latex.theory_entry name)), i + 1)
     7.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Mon Sep 19 16:18:34 2011 +0200
     7.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Mon Sep 19 22:48:05 2011 +0200
     7.3 @@ -12,11 +12,11 @@
     7.4  import scala.actors.Actor._
     7.5  import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment,
     7.6    ScrollPane, TabbedPane, Component, Swing}
     7.7 -import scala.swing.event.{ButtonClicked, SelectionChanged}
     7.8 +import scala.swing.event.{ButtonClicked, MouseClicked, SelectionChanged}
     7.9  
    7.10  import java.lang.System
    7.11  import java.awt.{BorderLayout, Graphics2D, Insets}
    7.12 -import javax.swing.{JList, DefaultListCellRenderer, UIManager}
    7.13 +import javax.swing.{JList, DefaultListCellRenderer, BorderFactory}
    7.14  import javax.swing.border.{BevelBorder, SoftBevelBorder}
    7.15  
    7.16  import org.gjt.sp.jedit.{View, jEdit}
    7.17 @@ -29,7 +29,14 @@
    7.18    private val readme = new HTML_Panel("SansSerif", 14)
    7.19    readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
    7.20  
    7.21 -  val status = new ListView(Nil: List[Document.Node.Name])
    7.22 +  val status = new ListView(Nil: List[Document.Node.Name]) {
    7.23 +    listenTo(mouse.clicks)
    7.24 +    reactions += {
    7.25 +      case MouseClicked(_, point, _, clicks, _) if clicks == 2 =>
    7.26 +        val index = peer.locationToIndex(point)
    7.27 +        if (index >= 0) jEdit.openFile(view, listData(index).node)
    7.28 +    }
    7.29 +  }
    7.30    status.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
    7.31    status.selection.intervalMode = ListView.IntervalMode.Single
    7.32  
    7.33 @@ -86,11 +93,11 @@
    7.34  
    7.35    private var nodes_status: Map[Document.Node.Name, Isar_Document.Node_Status] = Map.empty
    7.36  
    7.37 -  private class Node_Renderer_Component extends Label
    7.38 +  private object Node_Renderer_Component extends Label
    7.39    {
    7.40 +    opaque = false
    7.41      xAlignment = Alignment.Leading
    7.42 -    border = UIManager.getBorder("List.cellNoFocusBorder")
    7.43 -    val empty_insets = new Insets(0, 0, 0, 0)
    7.44 +    border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
    7.45  
    7.46      var node_name = Document.Node.Name.empty
    7.47      override def paintComponent(gfx: Graphics2D)
    7.48 @@ -98,7 +105,7 @@
    7.49        nodes_status.get(node_name) match {
    7.50          case Some(st) if st.total > 0 =>
    7.51            val size = peer.getSize()
    7.52 -          val insets = if (border == null) empty_insets else border.getBorderInsets(this.peer)
    7.53 +          val insets = border.getBorderInsets(this.peer)
    7.54            val w = size.width - insets.left - insets.right
    7.55            val h = size.height - insets.top - insets.bottom
    7.56            var end = size.width - insets.right
    7.57 @@ -119,18 +126,15 @@
    7.58      }
    7.59    }
    7.60  
    7.61 -  private class Node_Renderer extends
    7.62 -    ListView.AbstractRenderer[Document.Node.Name, Node_Renderer_Component](
    7.63 -      new Node_Renderer_Component)
    7.64 +  private class Node_Renderer extends ListView.Renderer[Document.Node.Name]
    7.65    {
    7.66 -    def configure(list: ListView[_], isSelected: Boolean, focused: Boolean,
    7.67 -      name: Document.Node.Name, index: Int)
    7.68 +    def componentFor(list: ListView[_], isSelected: Boolean, focused: Boolean,
    7.69 +      name: Document.Node.Name, index: Int): Component =
    7.70      {
    7.71 -      component.opaque = false
    7.72 -      component.background = list.background
    7.73 -      component.foreground = list.foreground
    7.74 +      val component = Node_Renderer_Component
    7.75        component.node_name = name
    7.76 -      component.text = name.theory + " "
    7.77 +      component.text = name.theory
    7.78 +      component
    7.79      }
    7.80    }
    7.81    status.renderer = new Node_Renderer