tuned signature;
authorwenzelm
Mon Mar 11 18:58:06 2019 +0100 (6 weeks ago ago)
changeset 70079990c6e8faf2c
parent 70078 a9849222844d
child 70080 27cf4287de43
tuned signature;
src/Tools/VSCode/src/vscode_rendering.scala
src/Tools/jEdit/src/jedit_rendering.scala
     1.1 --- a/src/Tools/VSCode/src/vscode_rendering.scala	Mon Mar 11 16:47:22 2019 +0100
     1.2 +++ b/src/Tools/VSCode/src/vscode_rendering.scala	Mon Mar 11 18:58:06 2019 +0100
     1.3 @@ -247,7 +247,7 @@
     1.4  
     1.5    /* tooltips */
     1.6  
     1.7 -  def timing_threshold: Double = options.real("vscode_timing_threshold")
     1.8 +  override def timing_threshold: Double = options.real("vscode_timing_threshold")
     1.9  
    1.10  
    1.11    /* hyperlinks */
     2.1 --- a/src/Tools/jEdit/src/jedit_rendering.scala	Mon Mar 11 16:47:22 2019 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit_rendering.scala	Mon Mar 11 18:58:06 2019 +0100
     2.3 @@ -291,7 +291,7 @@
     2.4    /* tooltips */
     2.5  
     2.6    def tooltip_margin: Int = options.int("jedit_tooltip_margin")
     2.7 -  def timing_threshold: Double = options.real("jedit_timing_threshold")
     2.8 +  override def timing_threshold: Double = options.real("jedit_timing_threshold")
     2.9  
    2.10    def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
    2.11      tooltips(Rendering.tooltip_elements, range).map(info => info.map(Pretty.fbreaks(_)))