src/Tools/jEdit/src/output_dockable.scala
author wenzelm
Wed, 08 Jun 2011 21:40:54 +0200
changeset 43286 a319da4fbfb0
parent 43282 5d294220ca43
child 43419 6ed49c52d463
permissions -rw-r--r--
simplified directory structure;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43282
5d294220ca43 moved sources -- eliminated Netbeans artifact of jedit package directory;
wenzelm
parents: 42978
diff changeset
     1
/*  Title:      Tools/jEdit/src/output_dockable.scala
36760
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     2
    Author:     Makarius
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     3
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     4
Dockable window with result message output.
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     5
*/
34408
ad7b6c4813c8 added some headers and comments;
wenzelm
parents: 34406
diff changeset
     6
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
     8
34760
dc7f5e0d9d27 misc modernization of names;
wenzelm
parents: 34759
diff changeset
     9
36015
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34871
diff changeset
    10
import isabelle._
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34871
diff changeset
    11
34768
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents: 34765
diff changeset
    12
import scala.actors.Actor._
34760
dc7f5e0d9d27 misc modernization of names;
wenzelm
parents: 34759
diff changeset
    13
37017
cf6625012282 try CheckBox instead of ToggleButton, which is visually confusing without window focus, e.g. in a floating instance (problem of MacOS look-and-feel);
wenzelm
parents: 37014
diff changeset
    14
import scala.swing.{FlowPanel, Button, CheckBox}
36988
fd641bc85222 basic controls to freeze/update prover results;
wenzelm
parents: 36817
diff changeset
    15
import scala.swing.event.ButtonClicked
fd641bc85222 basic controls to freeze/update prover results;
wenzelm
parents: 36817
diff changeset
    16
37067
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37048
diff changeset
    17
import java.awt.BorderLayout
37014
1af0f718ffdc handle component resize for output / HTML panel;
wenzelm
parents: 36993
diff changeset
    18
import java.awt.event.{ComponentEvent, ComponentAdapter}
34748
a2ed621f5f52 reduced logging;
wenzelm
parents: 34747
diff changeset
    19
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    20
import org.gjt.sp.jedit.View
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    21
34765
63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable;
wenzelm
parents: 34760
diff changeset
    22
37067
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37048
diff changeset
    23
class Output_Dockable(view: View, position: String) extends Dockable(view, position)
34760
dc7f5e0d9d27 misc modernization of names;
wenzelm
parents: 34759
diff changeset
    24
{
38223
2a368e8e0a80 more explicit treatment of Swing thread context;
wenzelm
parents: 38152
diff changeset
    25
  Swing_Thread.require()
37130
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
    26
39592
5638fe4f0843 tuned signature;
wenzelm
parents: 39518
diff changeset
    27
  private val html_panel =
37164
8b4617ad1593 reuse main view.font from jEdit;
wenzelm
parents: 37132
diff changeset
    28
    new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
42978
6b41a075251f adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents: 39592
diff changeset
    29
  {
6b41a075251f adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents: 39592
diff changeset
    30
    override val handler: PartialFunction[HTML_Panel.Event, Unit] = {
6b41a075251f adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents: 39592
diff changeset
    31
      case HTML_Panel.Mouse_Click(elem, event) if elem.getClassName() == "sendback" =>
6b41a075251f adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents: 39592
diff changeset
    32
        val text = elem.getFirstChild().getNodeValue()
6b41a075251f adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents: 39592
diff changeset
    33
6b41a075251f adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents: 39592
diff changeset
    34
        Document_View(view.getTextArea) match {
6b41a075251f adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents: 39592
diff changeset
    35
          case Some(doc_view) =>
6b41a075251f adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents: 39592
diff changeset
    36
            val cmd = current_command.get
6b41a075251f adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents: 39592
diff changeset
    37
            val start_ofs = doc_view.model.snapshot().node.command_start(cmd).get
6b41a075251f adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents: 39592
diff changeset
    38
            val buffer = view.getBuffer
6b41a075251f adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents: 39592
diff changeset
    39
            buffer.beginCompoundEdit()
6b41a075251f adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents: 39592
diff changeset
    40
            buffer.remove(start_ofs, cmd.length)
6b41a075251f adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents: 39592
diff changeset
    41
            buffer.insert(start_ofs, text)
6b41a075251f adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents: 39592
diff changeset
    42
            buffer.endCompoundEdit()
6b41a075251f adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents: 39592
diff changeset
    43
          case None =>
6b41a075251f adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents: 39592
diff changeset
    44
        }
6b41a075251f adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents: 39592
diff changeset
    45
    }       
6b41a075251f adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents: 39592
diff changeset
    46
  }
6b41a075251f adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
krauss
parents: 39592
diff changeset
    47
39518
wenzelm
parents: 39513
diff changeset
    48
  set_content(html_panel)
34768
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents: 34765
diff changeset
    49
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents: 34765
diff changeset
    50
37130
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
    51
  /* component state -- owned by Swing thread */
36988
fd641bc85222 basic controls to freeze/update prover results;
wenzelm
parents: 36817
diff changeset
    52
37019
8f747cee4e27 zoom font size;
wenzelm
parents: 37017
diff changeset
    53
  private var zoom_factor = 100
37131
d4697a30bd02 clarified auto_update vs. update;
wenzelm
parents: 37130
diff changeset
    54
  private var show_tracing = false
d4697a30bd02 clarified auto_update vs. update;
wenzelm
parents: 37130
diff changeset
    55
  private var follow_caret = true
d4697a30bd02 clarified auto_update vs. update;
wenzelm
parents: 37130
diff changeset
    56
  private var current_command: Option[Command] = None
37019
8f747cee4e27 zoom font size;
wenzelm
parents: 37017
diff changeset
    57
37131
d4697a30bd02 clarified auto_update vs. update;
wenzelm
parents: 37130
diff changeset
    58
d4697a30bd02 clarified auto_update vs. update;
wenzelm
parents: 37130
diff changeset
    59
  private def handle_resize()
d4697a30bd02 clarified auto_update vs. update;
wenzelm
parents: 37130
diff changeset
    60
  {
37019
8f747cee4e27 zoom font size;
wenzelm
parents: 37017
diff changeset
    61
    Swing_Thread.now {
37164
8b4617ad1593 reuse main view.font from jEdit;
wenzelm
parents: 37132
diff changeset
    62
      html_panel.resize(Isabelle.font_family(),
8b4617ad1593 reuse main view.font from jEdit;
wenzelm
parents: 37132
diff changeset
    63
        scala.math.round(Isabelle.font_size() * zoom_factor / 100))
37019
8f747cee4e27 zoom font size;
wenzelm
parents: 37017
diff changeset
    64
    }
37131
d4697a30bd02 clarified auto_update vs. update;
wenzelm
parents: 37130
diff changeset
    65
  }
36988
fd641bc85222 basic controls to freeze/update prover results;
wenzelm
parents: 36817
diff changeset
    66
37849
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37372
diff changeset
    67
  private def handle_perspective(): Boolean =
37131
d4697a30bd02 clarified auto_update vs. update;
wenzelm
parents: 37130
diff changeset
    68
    Swing_Thread.now {
d4697a30bd02 clarified auto_update vs. update;
wenzelm
parents: 37130
diff changeset
    69
      Document_View(view.getTextArea) match {
37849
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37372
diff changeset
    70
        case Some(doc_view) =>
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37372
diff changeset
    71
          val cmd = doc_view.selected_command()
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37372
diff changeset
    72
          if (current_command == cmd) false
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37372
diff changeset
    73
          else { current_command = cmd; true }
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37372
diff changeset
    74
        case None => false
37131
d4697a30bd02 clarified auto_update vs. update;
wenzelm
parents: 37130
diff changeset
    75
      }
d4697a30bd02 clarified auto_update vs. update;
wenzelm
parents: 37130
diff changeset
    76
    }
37130
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
    77
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
    78
  private def handle_update(restriction: Option[Set[Command]] = None)
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
    79
  {
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
    80
    Swing_Thread.now {
37849
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37372
diff changeset
    81
      if (follow_caret) handle_perspective()
37130
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
    82
      Document_View(view.getTextArea) match {
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
    83
        case Some(doc_view) =>
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
    84
          current_command match {
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
    85
            case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
38152
eab0d1c2e46e Change.Snapshot: include from_current/to_current here, with precomputed changes;
wenzelm
parents: 38151
diff changeset
    86
              val snapshot = doc_view.model.snapshot()
37130
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
    87
              val filtered_results =
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38360
diff changeset
    88
                snapshot.state(cmd).results.iterator.map(_._2) filter {
39513
fce2202892c4 discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
wenzelm
parents: 38872
diff changeset
    89
                  case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing  // FIXME not scalable
37130
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
    90
                  case _ => true
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
    91
                }
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38360
diff changeset
    92
              html_panel.render(filtered_results.toList)
37130
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
    93
            case _ =>
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
    94
          }
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
    95
        case None =>
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
    96
      }
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
    97
    }
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
    98
  }
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
    99
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
   100
37067
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37048
diff changeset
   101
  /* main actor */
34768
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents: 34765
diff changeset
   102
37067
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37048
diff changeset
   103
  private val main_actor = actor {
34768
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents: 34765
diff changeset
   104
    loop {
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents: 34765
diff changeset
   105
      react {
37019
8f747cee4e27 zoom font size;
wenzelm
parents: 37017
diff changeset
   106
        case Session.Global_Settings => handle_resize()
38360
53224a4d2f0e specific Session.Commands_Changed;
wenzelm
parents: 38356
diff changeset
   107
        case Session.Commands_Changed(changed) => handle_update(Some(changed))
37850
afb5653a3a47 observe follow_caret (again);
wenzelm
parents: 37849
diff changeset
   108
        case Session.Perspective => if (follow_caret && handle_perspective()) handle_update()
37067
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37048
diff changeset
   109
        case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
34768
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents: 34765
diff changeset
   110
      }
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents: 34765
diff changeset
   111
    }
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents: 34765
diff changeset
   112
  }
34428
d69fd18f37f9 basic setup of anti-aliasing, according to jEdit property;
wenzelm
parents: 34424
diff changeset
   113
37067
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37048
diff changeset
   114
  override def init()
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34775
diff changeset
   115
  {
37849
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37372
diff changeset
   116
    Isabelle.session.global_settings += main_actor
37129
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37067
diff changeset
   117
    Isabelle.session.commands_changed += main_actor
37849
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37372
diff changeset
   118
    Isabelle.session.perspective += main_actor
34768
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents: 34765
diff changeset
   119
  }
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents: 34765
diff changeset
   120
37067
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37048
diff changeset
   121
  override def exit()
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents: 34775
diff changeset
   122
  {
37849
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37372
diff changeset
   123
    Isabelle.session.global_settings -= main_actor
37129
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 37067
diff changeset
   124
    Isabelle.session.commands_changed -= main_actor
37849
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37372
diff changeset
   125
    Isabelle.session.perspective -= main_actor
34768
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents: 34765
diff changeset
   126
  }
36988
fd641bc85222 basic controls to freeze/update prover results;
wenzelm
parents: 36817
diff changeset
   127
fd641bc85222 basic controls to freeze/update prover results;
wenzelm
parents: 36817
diff changeset
   128
37014
1af0f718ffdc handle component resize for output / HTML panel;
wenzelm
parents: 36993
diff changeset
   129
  /* resize */
1af0f718ffdc handle component resize for output / HTML panel;
wenzelm
parents: 36993
diff changeset
   130
1af0f718ffdc handle component resize for output / HTML panel;
wenzelm
parents: 36993
diff changeset
   131
  addComponentListener(new ComponentAdapter {
37849
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37372
diff changeset
   132
    val delay = Swing_Thread.delay_last(Isabelle.session.update_delay) { handle_resize() }
37014
1af0f718ffdc handle component resize for output / HTML panel;
wenzelm
parents: 36993
diff changeset
   133
    override def componentResized(e: ComponentEvent) { delay() }
1af0f718ffdc handle component resize for output / HTML panel;
wenzelm
parents: 36993
diff changeset
   134
  })
1af0f718ffdc handle component resize for output / HTML panel;
wenzelm
parents: 36993
diff changeset
   135
1af0f718ffdc handle component resize for output / HTML panel;
wenzelm
parents: 36993
diff changeset
   136
37130
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
   137
  /* controls */
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
   138
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
   139
  private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
   140
  zoom.tooltip = "Zoom factor for basic font size"
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
   141
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
   142
  private val tracing = new CheckBox("Tracing") {
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
   143
    reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() }
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
   144
  }
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
   145
  tracing.selected = show_tracing
37372
babe498016e8 tuned tooltips;
wenzelm
parents: 37164
diff changeset
   146
  tracing.tooltip = "Indicate output of tracing messages"
37130
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
   147
37131
d4697a30bd02 clarified auto_update vs. update;
wenzelm
parents: 37130
diff changeset
   148
  private val auto_update = new CheckBox("Auto update") {
37130
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
   149
    reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() }
7f18edbbf618 more reactive message handling, notably for follow_caret mode;
wenzelm
parents: 37129
diff changeset
   150
  }
37131
d4697a30bd02 clarified auto_update vs. update;
wenzelm
parents: 37130
diff changeset
   151
  auto_update.selected = follow_caret
37372
babe498016e8 tuned tooltips;
wenzelm
parents: 37164
diff changeset
   152
  auto_update.tooltip = "Indicate automatic update following cursor movement"
36988
fd641bc85222 basic controls to freeze/update prover results;
wenzelm
parents: 36817
diff changeset
   153
37131
d4697a30bd02 clarified auto_update vs. update;
wenzelm
parents: 37130
diff changeset
   154
  private val update = new Button("Update") {
37849
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37372
diff changeset
   155
    reactions += { case ButtonClicked(_) => handle_perspective(); handle_update() }
37131
d4697a30bd02 clarified auto_update vs. update;
wenzelm
parents: 37130
diff changeset
   156
  }
37372
babe498016e8 tuned tooltips;
wenzelm
parents: 37164
diff changeset
   157
  update.tooltip = "Update display according to the command at cursor position"
37131
d4697a30bd02 clarified auto_update vs. update;
wenzelm
parents: 37130
diff changeset
   158
39592
5638fe4f0843 tuned signature;
wenzelm
parents: 39518
diff changeset
   159
  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update)
37039
d01da9438170 added checkboxes for debug/tracing filter;
wenzelm
parents: 37037
diff changeset
   160
  add(controls.peer, BorderLayout.NORTH)
d01da9438170 added checkboxes for debug/tracing filter;
wenzelm
parents: 37037
diff changeset
   161
36988
fd641bc85222 basic controls to freeze/update prover results;
wenzelm
parents: 36817
diff changeset
   162
  handle_update()
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   163
}