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);
authorwenzelm
Fri Sep 17 22:17:57 2010 +0200 (2010-09-17 ago)
changeset 39513fce2202892c4
parent 39512 31290f54be19
child 39514 d9cf3f833318
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);
NEWS
src/Pure/General/markup.scala
src/Pure/Isar/runtime.ML
src/Pure/Isar/toplevel.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/System/isabelle_process.ML
src/Pure/System/isabelle_process.scala
src/Tools/jEdit/dist-template/etc/isabelle-jedit.css
src/Tools/jEdit/src/jedit/output_dockable.scala
     1.1 --- a/NEWS	Fri Sep 17 21:50:44 2010 +0200
     1.2 +++ b/NEWS	Fri Sep 17 22:17:57 2010 +0200
     1.3 @@ -244,6 +244,9 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Discontinued Output.debug.  Minor INCOMPATIBILITY, use plain writeln
     1.8 +instead (or tracing for high-volume output).
     1.9 +
    1.10  * Configuration option show_question_marks only affects regular pretty
    1.11  printing of types and terms, not raw Term.string_of_vname.
    1.12  
     2.1 --- a/src/Pure/General/markup.scala	Fri Sep 17 21:50:44 2010 +0200
     2.2 +++ b/src/Pure/General/markup.scala	Fri Sep 17 22:17:57 2010 +0200
     2.3 @@ -239,7 +239,6 @@
     2.4    val TRACING = "tracing"
     2.5    val WARNING = "warning"
     2.6    val ERROR = "error"
     2.7 -  val DEBUG = "debug"
     2.8    val SYSTEM = "system"
     2.9    val INPUT = "input"
    2.10    val STDIN = "stdin"
     3.1 --- a/src/Pure/Isar/runtime.ML	Fri Sep 17 21:50:44 2010 +0200
     3.2 +++ b/src/Pure/Isar/runtime.ML	Fri Sep 17 22:17:57 2010 +0200
     3.3 @@ -10,6 +10,7 @@
     3.4    exception TERMINATE
     3.5    exception EXCURSION_FAIL of exn * string
     3.6    exception TOPLEVEL_ERROR
     3.7 +  val debug: bool Unsynchronized.ref
     3.8    val exn_context: Proof.context option -> exn -> exn
     3.9    val exn_messages: (exn -> Position.T) -> exn -> string list
    3.10    val exn_message: (exn -> Position.T) -> exn -> string
    3.11 @@ -28,6 +29,8 @@
    3.12  exception EXCURSION_FAIL of exn * string;
    3.13  exception TOPLEVEL_ERROR;
    3.14  
    3.15 +val debug = Unsynchronized.ref false;
    3.16 +
    3.17  
    3.18  (* exn_context *)
    3.19  
    3.20 @@ -52,7 +55,7 @@
    3.21          | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
    3.22        end;
    3.23  
    3.24 -    val detailed = ! Output.debugging;
    3.25 +    val detailed = ! debug;
    3.26  
    3.27      fun exn_msgs context exn =
    3.28        if Exn.is_interrupt exn then []
    3.29 @@ -94,11 +97,10 @@
    3.30    | msgs => cat_lines msgs);
    3.31  
    3.32  
    3.33 -
    3.34  (** controlled execution **)
    3.35  
    3.36  fun debugging f x =
    3.37 -  if ! Output.debugging then
    3.38 +  if ! debug then
    3.39      Exn.release (exception_trace (fn () =>
    3.40        Exn.Result (f x) handle
    3.41          exn as UNDEF => Exn.Exn exn
     4.1 --- a/src/Pure/Isar/toplevel.ML	Fri Sep 17 21:50:44 2010 +0200
     4.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Sep 17 22:17:57 2010 +0200
     4.3 @@ -215,7 +215,7 @@
     4.4  (** toplevel transitions **)
     4.5  
     4.6  val quiet = Unsynchronized.ref false;
     4.7 -val debug = Output.debugging;
     4.8 +val debug = Runtime.debug;
     4.9  val interact = Unsynchronized.ref false;
    4.10  val timing = Output.timing;
    4.11  val profiling = Unsynchronized.ref 0;
     5.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Sep 17 21:50:44 2010 +0200
     5.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Sep 17 22:17:57 2010 +0200
     5.3 @@ -79,7 +79,6 @@
     5.4    Output.report_fn := (fn _ => ());
     5.5    Output.priority_fn := message (special "I") (special "J") "";
     5.6    Output.tracing_fn := message (special "I" ^ special "V") (special "J") "";
     5.7 -  Output.debug_fn := message (special "K") (special "L") "+++ ";
     5.8    Output.warning_fn := message (special "K") (special "L") "### ";
     5.9    Output.error_fn := message (special "M") (special "N") "*** ";
    5.10    Output.prompt_fn := (fn s => Output.std_output (render s ^ special "S")));
     6.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Sep 17 21:50:44 2010 +0200
     6.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Sep 17 22:17:57 2010 +0200
     6.3 @@ -166,8 +166,7 @@
     6.4    Output.priority_fn := (fn s => normalmsg Status s);
     6.5    Output.tracing_fn := (fn s => normalmsg Tracing s);
     6.6    Output.warning_fn := (fn s => errormsg Message Warning s);
     6.7 -  Output.error_fn := (fn s => errormsg Message Fatal s);
     6.8 -  Output.debug_fn := (fn s => errormsg Message Debug s));
     6.9 +  Output.error_fn := (fn s => errormsg Message Fatal s));
    6.10  
    6.11  
    6.12  (* immediate messages *)
     7.1 --- a/src/Pure/System/isabelle_process.ML	Fri Sep 17 21:50:44 2010 +0200
     7.2 +++ b/src/Pure/System/isabelle_process.ML	Fri Sep 17 22:17:57 2010 +0200
     7.3 @@ -109,7 +109,6 @@
     7.4      Output.tracing_fn  := standard_message out_stream true "E";
     7.5      Output.warning_fn  := standard_message out_stream true "F";
     7.6      Output.error_fn    := standard_message out_stream true "G";
     7.7 -    Output.debug_fn    := standard_message out_stream true "H";
     7.8      Output.priority_fn := ! Output.writeln_fn;
     7.9      Output.prompt_fn   := ignore;
    7.10      (in_stream, out_stream)
     8.1 --- a/src/Pure/System/isabelle_process.scala	Fri Sep 17 21:50:44 2010 +0200
     8.2 +++ b/src/Pure/System/isabelle_process.scala	Fri Sep 17 22:17:57 2010 +0200
     8.3 @@ -28,8 +28,7 @@
     8.4        ('D' : Int) -> Markup.WRITELN,
     8.5        ('E' : Int) -> Markup.TRACING,
     8.6        ('F' : Int) -> Markup.WARNING,
     8.7 -      ('G' : Int) -> Markup.ERROR,
     8.8 -      ('H' : Int) -> Markup.DEBUG)
     8.9 +      ('G' : Int) -> Markup.ERROR)
    8.10      def is_raw(kind: String) =
    8.11        kind == Markup.STDOUT
    8.12      def is_control(kind: String) =
     9.1 --- a/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Fri Sep 17 21:50:44 2010 +0200
     9.2 +++ b/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Fri Sep 17 22:17:57 2010 +0200
     9.3 @@ -6,7 +6,6 @@
     9.4  .tracing { background-color: #F0F8FF; }
     9.5  .warning { background-color: #EEE8AA; }
     9.6  .error { background-color: #FFC1C1; }
     9.7 -.debug { background-color: #FFE4E1; }
     9.8  
     9.9  .report { display: none; }
    9.10  
    10.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Fri Sep 17 21:50:44 2010 +0200
    10.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Fri Sep 17 22:17:57 2010 +0200
    10.3 @@ -32,7 +32,6 @@
    10.4    /* component state -- owned by Swing thread */
    10.5  
    10.6    private var zoom_factor = 100
    10.7 -  private var show_debug = false
    10.8    private var show_tracing = false
    10.9    private var follow_caret = true
   10.10    private var current_command: Option[Command] = None
   10.11 @@ -68,8 +67,7 @@
   10.12                val snapshot = doc_view.model.snapshot()
   10.13                val filtered_results =
   10.14                  snapshot.state(cmd).results.iterator.map(_._2) filter {
   10.15 -                  case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing
   10.16 -                  case XML.Elem(Markup(Markup.DEBUG, _), _) => show_debug
   10.17 +                  case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing  // FIXME not scalable
   10.18                    case _ => true
   10.19                  }
   10.20                html_panel.render(filtered_results.toList)
   10.21 @@ -122,13 +120,6 @@
   10.22    private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
   10.23    zoom.tooltip = "Zoom factor for basic font size"
   10.24  
   10.25 -  private val debug = new CheckBox("Debug") {
   10.26 -    reactions += { case ButtonClicked(_) => show_debug = this.selected; handle_update() }
   10.27 -  }
   10.28 -  debug.selected = show_debug
   10.29 -  debug.tooltip =
   10.30 -    "<html>Indicate output of debug messages<br>(also needs to be enabled on the prover side)</html>"
   10.31 -
   10.32    private val tracing = new CheckBox("Tracing") {
   10.33      reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() }
   10.34    }
   10.35 @@ -146,7 +137,7 @@
   10.36    }
   10.37    update.tooltip = "Update display according to the command at cursor position"
   10.38  
   10.39 -  val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, debug, tracing, auto_update, update)
   10.40 +  val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update)
   10.41    add(controls.peer, BorderLayout.NORTH)
   10.42  
   10.43    handle_update()