--- a/src/HOL/ROOT Sat Jan 12 16:49:40 2013 +0100
+++ b/src/HOL/ROOT Sat Jan 12 20:42:20 2013 +0100
@@ -16,7 +16,7 @@
"Tools/Quickcheck/Narrowing_Engine.hs"
"Tools/Quickcheck/PNF_Narrowing_Engine.hs"
-session "HOL-Library" in Library = HOL +
+session "HOL-Library" (main) in Library = HOL +
description {* Classical Higher-order Logic -- batteries included *}
theories
Library
@@ -178,7 +178,7 @@
options [document = false]
theories [quick_and_dirty] Nitpick_Examples
-session "HOL-Algebra" in Algebra = HOL +
+session "HOL-Algebra" (main) in Algebra = HOL +
description {*
Author: Clemens Ballarin, started 24 September 1999
@@ -553,7 +553,7 @@
theories [proofs = 0] (* FIXME !? *)
ATP_Problem_Import
-session "HOL-Multivariate_Analysis" in Multivariate_Analysis = HOL +
+session "HOL-Multivariate_Analysis" (main) in Multivariate_Analysis = HOL +
options [document_graph]
theories
Multivariate_Analysis
@@ -620,7 +620,7 @@
Misc_Codata
Misc_Data
-session "HOL-Word" in Word = HOL +
+session "HOL-Word" (main) in Word = HOL +
options [document_graph]
theories Word
files "document/root.bib" "document/root.tex"
@@ -680,7 +680,7 @@
"VCC_Max.b2i"
"VCC_Max.certs"
-session "HOL-SPARK" in "SPARK" = "HOL-Word" +
+session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
options [document = false]
theories SPARK
--- a/src/Pure/General/file.scala Sat Jan 12 16:49:40 2013 +0100
+++ b/src/Pure/General/file.scala Sat Jan 12 20:42:20 2013 +0100
@@ -75,6 +75,21 @@
def read_gzip(path: Path): String = read_gzip(path.file)
+ /* read lines */
+
+ def read_lines(reader: BufferedReader, progress: String => Unit): List[String] =
+ {
+ val result = new mutable.ListBuffer[String]
+ var line: String = null
+ while ({ line = reader.readLine; line != null }) {
+ progress(line)
+ result += line
+ }
+ reader.close
+ result.toList
+ }
+
+
/* try_read */
def try_read(paths: Seq[Path]): String =
--- a/src/Pure/General/pretty.scala Sat Jan 12 16:49:40 2013 +0100
+++ b/src/Pure/General/pretty.scala Sat Jan 12 20:42:20 2013 +0100
@@ -14,7 +14,6 @@
{
/* spaces */
- val spc = ' '
val space = " "
private val static_spaces = space * 4000
@@ -84,10 +83,13 @@
private val margin_default = 76
private def metric_default(s: String) = s.length.toDouble
+ def char_width(metrics: FontMetrics): Double = metrics.stringWidth("mix").toDouble / 3
+ def char_width_int(metrics: FontMetrics): Int = char_width(metrics).round.toInt
+
def font_metric(metrics: FontMetrics): String => Double =
if (metrics == null) ((s: String) => s.length.toDouble)
else {
- val unit = metrics.charWidth(spc).toDouble
+ val unit = char_width(metrics)
((s: String) => if (s == "\n") 1.0 else metrics.stringWidth(s) / unit)
}
--- a/src/Pure/General/properties.ML Sat Jan 12 16:49:40 2013 +0100
+++ b/src/Pure/General/properties.ML Sat Jan 12 20:42:20 2013 +0100
@@ -6,17 +6,19 @@
signature PROPERTIES =
sig
- type T = (string * string) list
+ type entry = string * string
+ type T = entry list
val defined: T -> string -> bool
val get: T -> string -> string option
- val put: string * string -> T -> T
+ val put: entry -> T -> T
val remove: string -> T -> T
end;
structure Properties: PROPERTIES =
struct
-type T = (string * string) list;
+type entry = string * string;
+type T = entry list;
fun defined (props: T) name = AList.defined (op =) props name;
fun get (props: T) name = AList.lookup (op =) props name;
--- a/src/Pure/General/properties.scala Sat Jan 12 16:49:40 2013 +0100
+++ b/src/Pure/General/properties.scala Sat Jan 12 20:42:20 2013 +0100
@@ -126,8 +126,7 @@
}
def parse_lines(prefix: java.lang.String, lines: List[java.lang.String]): List[T] =
- for (line <- lines if line.startsWith(prefix))
- yield parse(line.substring(prefix.length))
+ for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse(s)
def find_parse_line(prefix: java.lang.String, lines: List[java.lang.String]): Option[T] =
lines.find(_.startsWith(prefix)).map(line => parse(line.substring(prefix.length)))
--- a/src/Pure/PIDE/markup.ML Sat Jan 12 16:49:40 2013 +0100
+++ b/src/Pure/PIDE/markup.ML Sat Jan 12 20:42:20 2013 +0100
@@ -125,14 +125,16 @@
val graphviewN: string
val sendbackN: string
val paddingN: string
- val padding_line: string * string
+ val padding_line: Properties.entry
val dialogN: string val dialog: serial -> string -> T
val functionN: string
val assign_execs: Properties.T
val removed_versions: Properties.T
val invoke_scala: string -> string -> Properties.T
val cancel_scala: string -> Properties.T
- val ML_statistics: string * string
+ val ML_statistics: Properties.entry
+ val loading_theory: string -> Properties.T
+ val dest_loading_theory: Properties.T -> string option
val no_output: Output.output * Output.output
val default_output: T -> Output.output * Output.output
val add_mode: string -> (T -> Output.output * Output.output) -> unit
@@ -408,6 +410,11 @@
val ML_statistics = (functionN, "ML_statistics");
+fun loading_theory name = [("function", "loading_theory"), ("name", name)];
+
+fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
+ | dest_loading_theory _ = NONE;
+
(** print mode operations **)
--- a/src/Pure/System/isabelle_system.ML Sat Jan 12 16:49:40 2013 +0100
+++ b/src/Pure/System/isabelle_system.ML Sat Jan 12 20:42:20 2013 +0100
@@ -14,7 +14,6 @@
val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a
val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
val with_tmp_fifo: (Path.T -> 'a) -> 'a
- val bash_output_fifo: string -> (Path.T -> 'a) -> 'a
val bash_output: string -> string * int
val bash: string -> int
end;
@@ -99,15 +98,5 @@
(_, 0) => f path
| (out, _) => error (trim_line out)));
-(* FIXME blocks on Cygwin 1.7.x *)
-(* See also http://cygwin.com/ml/cygwin/2010-08/msg00459.html *)
-fun bash_output_fifo script f =
- with_tmp_fifo (fn fifo =>
- uninterruptible (fn restore_attributes => fn () =>
- (case Bash.process (script ^ " > " ^ File.shell_path fifo ^ " &") of
- {rc = 0, terminate, ...} =>
- (restore_attributes f fifo handle exn => (terminate (); reraise exn))
- | {out, ...} => error (trim_line out))) ());
-
end;
--- a/src/Pure/System/isabelle_system.scala Sat Jan 12 16:49:40 2013 +0100
+++ b/src/Pure/System/isabelle_system.scala Sat Jan 12 20:42:20 2013 +0100
@@ -16,7 +16,6 @@
import scala.io.Source
import scala.util.matching.Regex
-import scala.collection.mutable
object Isabelle_System
@@ -331,24 +330,35 @@
/* bash */
- def bash_env(cwd: JFile, env: Map[String, String], script: String): (String, String, Int) =
+ final case class Bash_Result(out_lines: List[String], err_lines: List[String], rc: Int)
+ {
+ def out: String = cat_lines(out_lines)
+ def err: String = cat_lines(err_lines)
+ def add_err(s: String): Bash_Result = copy(err_lines = err_lines ::: List(s))
+ }
+
+ def bash_env(cwd: JFile, env: Map[String, String], script: String,
+ out_progress: String => Unit = (_: String) => (),
+ err_progress: String => Unit = (_: String) => ()): Bash_Result =
{
File.with_tmp_file("isabelle_script") { script_file =>
File.write(script_file, script)
val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file))
proc.stdin.close
- val (_, stdout) = Simple_Thread.future("bash_stdout") { File.read_stream(proc.stdout) }
- val (_, stderr) = Simple_Thread.future("bash_stderr") { File.read_stream(proc.stderr) }
+ val (_, stdout) =
+ Simple_Thread.future("bash_stdout") { File.read_lines(proc.stdout, out_progress) }
+ val (_, stderr) =
+ Simple_Thread.future("bash_stderr") { File.read_lines(proc.stderr, err_progress) }
val rc =
try { proc.join }
catch { case e: InterruptedException => Thread.interrupted; proc.terminate; 130 }
- (stdout.join, stderr.join, rc)
+ Bash_Result(stdout.join, stderr.join, rc)
}
}
- def bash(script: String): (String, String, Int) = bash_env(null, null, script)
+ def bash(script: String): Bash_Result = bash_env(null, null, script)
/* system tools */
--- a/src/Pure/System/system_channel.scala Sat Jan 12 16:49:40 2013 +0100
+++ b/src/Pure/System/system_channel.scala Sat Jan 12 20:42:20 2013 +0100
@@ -45,8 +45,8 @@
"FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" +
"echo -n \"$FIFO\"\n" +
"mkfifo -m 600 \"$FIFO\"\n"
- val (out, err, rc) = Isabelle_System.bash(script)
- if (rc == 0) out else error(err.trim)
+ val result = Isabelle_System.bash(script)
+ if (result.rc == 0) result.out else error(result.err)
}
private def rm_fifo(fifo: String): Boolean = (new JFile(fifo)).delete
--- a/src/Pure/Thy/thy_info.ML Sat Jan 12 16:49:40 2013 +0100
+++ b/src/Pure/Thy/thy_info.ML Sat Jan 12 20:42:20 2013 +0100
@@ -224,6 +224,7 @@
let
val _ = kill_thy name;
val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
+ val _ = Output.protocol_message (Markup.loading_theory name) "" handle Fail _ => ();
val {master = (thy_path, _), imports} = deps;
val dir = Path.dir thy_path;
--- a/src/Pure/Tools/build.ML Sat Jan 12 16:49:40 2013 +0100
+++ b/src/Pure/Tools/build.ML Sat Jan 12 20:42:20 2013 +0100
@@ -22,7 +22,10 @@
fun protocol_message props output =
(case ML_statistics props output of
SOME stats => writeln ("\fML_statistics = " ^ ML_Syntax.print_properties stats)
- | NONE => raise Fail "Undefined Output.protocol_message");
+ | NONE =>
+ (case Markup.dest_loading_theory props of
+ SOME name => writeln ("\floading_theory = " ^ name)
+ | NONE => raise Fail "Undefined Output.protocol_message"));
(* build *)
--- a/src/Pure/Tools/build.scala Sat Jan 12 16:49:40 2013 +0100
+++ b/src/Pure/Tools/build.scala Sat Jan 12 20:42:20 2013 +0100
@@ -21,15 +21,20 @@
{
/** progress context **/
- class Progress {
+ class Progress
+ {
def echo(msg: String) {}
+ def theory(session: String, theory: String) {}
def stopped: Boolean = false
}
object Ignore_Progress extends Progress
- object Console_Progress extends Progress {
+ class Console_Progress(verbose: Boolean) extends Progress
+ {
override def echo(msg: String) { java.lang.System.out.println(msg) }
+ override def theory(session: String, theory: String): Unit =
+ if (verbose) echo(session + ": theory " + theory)
}
@@ -412,7 +417,8 @@
/* jobs */
- private class Job(name: String, val info: Session_Info, output: Path, do_output: Boolean,
+ private class Job(progress: Build.Progress,
+ name: String, val info: Session_Info, output: Path, do_output: Boolean,
verbose: Boolean, browser_info: Path)
{
// global browser info dir
@@ -479,7 +485,14 @@
}
private val (thread, result) =
- Simple_Thread.future("build") { Isabelle_System.bash_env(info.dir.file, env, script) }
+ Simple_Thread.future("build") {
+ Isabelle_System.bash_env(info.dir.file, env, script,
+ out_progress = (line: String) =>
+ Library.try_unprefix("\floading_theory = ", line) match {
+ case Some(theory) => progress.theory(name, theory)
+ case None =>
+ })
+ }
def terminate: Unit = thread.interrupt
def is_finished: Boolean = result.is_finished
@@ -494,17 +507,16 @@
}
else None
- def join: (String, String, Int) = {
- val (out, err, rc) = result.join
+ def join: Isabelle_System.Bash_Result =
+ {
+ val res = result.join
+
args_file.delete
timer.map(_.cancel())
- val err1 =
- if (rc == 130)
- (if (err.isEmpty || err.endsWith("\n")) err else err + "\n") +
- (if (timeout) "*** Timeout\n" else "*** Interrupt\n")
- else err
- (out, err1, rc)
+ if (res.rc == 130)
+ res.add_err(if (timeout) "*** Timeout" else "*** Interrupt")
+ else res
}
}
@@ -634,22 +646,21 @@
case Some((name, (parent_heap, job))) =>
//{{{ finish job
- val (out, err, rc) = job.join
- val out_lines = split_lines(out)
- progress.echo(Library.trim_line(err))
+ val res = job.join
+ progress.echo(res.err)
val (parent_path, heap) =
- if (rc == 0) {
+ if (res.rc == 0) {
(output_dir + log(name)).file.delete
val sources = make_stamp(name)
val heap = heap_stamp(job.output_path)
File.write_gzip(output_dir + log_gz(name),
- sources + "\n" + parent_heap + "\n" + heap + "\n" + out)
+ sources + "\n" + parent_heap + "\n" + heap + "\n" + res.out)
val parent_path =
if (job.info.options.bool("browser_info"))
- out_lines.find(_.startsWith(SESSION_PARENT_PATH)).map(line =>
+ res.out_lines.find(_.startsWith(SESSION_PARENT_PATH)).map(line =>
line.substring(SESSION_PARENT_PATH.length))
else None
@@ -659,11 +670,11 @@
(output_dir + Path.basic(name)).file.delete
(output_dir + log_gz(name)).file.delete
- File.write(output_dir + log(name), out)
+ File.write(output_dir + log(name), res.out)
progress.echo(name + " FAILED")
- if (rc != 130) {
+ if (res.rc != 130) {
progress.echo("(see also " + (output_dir + log(name)).file.toString + ")")
- val lines = out_lines.filterNot(_.startsWith("\f"))
+ val lines = res.out_lines.filterNot(_.startsWith("\f"))
val tail = lines.drop(lines.length - 20 max 0)
progress.echo("\n" + cat_lines(tail))
}
@@ -671,7 +682,7 @@
(None, no_heap)
}
loop(pending - name, running - name,
- results + (name -> Result(false, parent_path, heap, rc)))
+ results + (name -> Result(false, parent_path, heap, res.rc)))
//}}}
case None if (running.size < (max_jobs max 1)) =>
//{{{ check/start next job
@@ -709,7 +720,7 @@
}
else if (parent_result.rc == 0) {
progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
- val job = new Job(name, info, output, do_output, verbose, browser_info)
+ val job = new Job(progress, name, info, output, do_output, verbose, browser_info)
loop(pending, running + (name -> (parent_result.heap, job)), results)
}
else {
@@ -769,9 +780,9 @@
val dirs =
select_dirs.map(d => (true, Path.explode(d))) :::
include_dirs.map(d => (false, Path.explode(d)))
- build(Build.Console_Progress, options, requirements, all_sessions, build_heap,
- clean_build, dirs, session_groups, max_jobs, list_files, no_build, system_mode,
- verbose, sessions)
+ build(new Build.Console_Progress(verbose), options, requirements, all_sessions,
+ build_heap, clean_build, dirs, session_groups, max_jobs, list_files, no_build,
+ system_mode, verbose, sessions)
case _ => error("Bad arguments:\n" + cat_lines(args))
}
}
--- a/src/Pure/Tools/build_dialog.scala Sat Jan 12 16:49:40 2013 +0100
+++ b/src/Pure/Tools/build_dialog.scala Sat Jan 12 20:42:20 2013 +0100
@@ -75,34 +75,52 @@
/* text */
val text = new TextArea {
- font = new Font("SansSerif", Font.PLAIN, 14)
+ font = new Font("SansSerif", Font.PLAIN, Library.resolution_scale(10))
editable = false
- columns = 40
- rows = 10
+ columns = 50
+ rows = 20
}
val progress = new Build.Progress
{
- override def echo(msg: String): Unit = Swing_Thread.now { text.append(msg + "\n") }
+ override def echo(msg: String): Unit =
+ Swing_Thread.later { text.append(msg + "\n") }
+ override def theory(session: String, theory: String): Unit =
+ echo(session + ": theory " + theory)
override def stopped: Boolean =
Swing_Thread.now { val b = is_stopped; is_stopped = false; b }
}
- /* action button */
+ /* action panel */
+
+ var do_auto_close = true
+ def check_auto_close(): Unit = if (do_auto_close && return_code == 0) sys.exit(return_code)
+
+ val auto_close = new CheckBox("Auto close") {
+ reactions += {
+ case ButtonClicked(_) => do_auto_close = this.selected
+ check_auto_close()
+ }
+ }
+ auto_close.selected = do_auto_close
+ auto_close.tooltip = "Automatically close dialog when finished"
+
var button_action: () => Unit = (() => is_stopped = true)
val button = new Button("Cancel") {
reactions += { case ButtonClicked(_) => button_action() }
}
- def button_exit(rc: Int)
+ def button_exit()
{
- button.text = if (rc == 0) "OK" else "Exit"
- button_action = (() => sys.exit(rc))
+ check_auto_close()
+ button.text = if (return_code == 0) "OK" else "Exit"
+ button_action = (() => sys.exit(return_code))
button.peer.getRootPane.setDefaultButton(button.peer)
}
- val action_panel = new FlowPanel(FlowPanel.Alignment.Center)(button)
+
+ val action_panel = new FlowPanel(FlowPanel.Alignment.Center)(button, auto_close)
/* layout panel */
@@ -130,7 +148,7 @@
Swing_Thread.now {
progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
return_code = rc
- button_exit(rc)
+ button_exit()
}
})
}
--- a/src/Pure/library.scala Sat Jan 12 16:49:40 2013 +0100
+++ b/src/Pure/library.scala Sat Jan 12 20:42:20 2013 +0100
@@ -11,7 +11,7 @@
import java.lang.System
import java.util.Locale
import java.util.concurrent.{Future => JFuture, TimeUnit}
-import java.awt.Component
+import java.awt.{Component, Toolkit}
import javax.swing.JOptionPane
import scala.swing.{ComboBox, TextArea, ScrollPane}
@@ -82,9 +82,8 @@
else ""
}
- def trim_line(str: String): String =
- if (str.endsWith("\n")) str.substring(0, str.length - 1)
- else str
+
+ /* strings */
def lowercase(str: String): String = str.toLowerCase(Locale.ENGLISH)
def uppercase(str: String): String = str.toUpperCase(Locale.ENGLISH)
@@ -93,6 +92,9 @@
if (str.length == 0) str
else uppercase(str.substring(0, 1)) + str.substring(1)
+ def try_unprefix(prfx: String, s: String): Option[String] =
+ if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None
+
/* quote */
@@ -198,6 +200,12 @@
}
+ /* screen resolution */
+
+ def resolution_scale(): Double = Toolkit.getDefaultToolkit.getScreenResolution.toDouble / 72
+ def resolution_scale(i: Int): Int = (i.toDouble * resolution_scale()).round.toInt
+
+
/* Java futures */
def future_value[A](x: A) = new JFuture[A]
--- a/src/Tools/jEdit/src/jedit_lib.scala Sat Jan 12 16:49:40 2013 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Sat Jan 12 20:42:20 2013 +0100
@@ -160,17 +160,6 @@
}
- /* char width */
-
- def char_width(text_area: TextArea): Int =
- {
- val painter = text_area.getPainter
- val font = painter.getFont
- val font_context = painter.getFontRenderContext
- font.getStringBounds(" ", font_context).getWidth.round.toInt
- }
-
-
/* graphics range */
case class Gfx_Range(val x: Int, val y: Int, val length: Int)
@@ -179,6 +168,8 @@
// NB: last line lacks \n
def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
{
+ val char_width = Pretty.char_width_int(text_area.getPainter.getFontMetrics)
+
val buffer = text_area.getBuffer
val p = text_area.offsetToXY(range.start)
@@ -186,9 +177,9 @@
val end = buffer.getLength
val stop = range.stop
val (q, r) =
- if (stop >= end) (text_area.offsetToXY(end), char_width(text_area) * (stop - end))
+ if (stop >= end) (text_area.offsetToXY(end), char_width * (stop - end))
else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
- (text_area.offsetToXY(stop - 1), char_width(text_area))
+ (text_area.offsetToXY(stop - 1), char_width)
else (text_area.offsetToXY(stop), 0)
if (p != null && q != null && p.x < q.x + r && p.y == q.y)
--- a/src/Tools/jEdit/src/pretty_text_area.scala Sat Jan 12 16:49:40 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Sat Jan 12 20:42:20 2013 +0100
@@ -107,13 +107,12 @@
getGutter.setGutterEnabled(jEdit.getBooleanProperty("view.gutter.enabled"))
- val font_metrics = getPainter.getFontMetrics(font)
- val margin =
- ((getWidth - getGutter.getWidth) / (font_metrics.charWidth(Pretty.spc) max 1) - 2) max 20
+ val fm = getPainter.getFontMetrics
+ val margin = ((getWidth - getGutter.getWidth) / (Pretty.char_width_int(fm) max 1) - 2) max 20
val base_snapshot = current_base_snapshot
val base_results = current_base_results
- val formatted_body = Pretty.formatted(current_body, margin, Pretty.font_metric(font_metrics))
+ val formatted_body = Pretty.formatted(current_body, margin, Pretty.font_metric(fm))
future_rendering.map(_.cancel(true))
future_rendering = Some(default_thread_pool.submit(() =>
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Sat Jan 12 16:49:40 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Sat Jan 12 20:42:20 2013 +0100
@@ -96,17 +96,15 @@
val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
{
- val font_metrics = pretty_text_area.getPainter.getFontMetrics
+ val fm = pretty_text_area.getPainter.getFontMetrics
val margin = rendering.tooltip_margin
val lines =
- XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(font_metrics)))(0)(
+ XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(fm)))(0)(
(n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
val bounds = rendering.tooltip_bounds
- val w =
- (font_metrics.charWidth(Pretty.spc) * (margin + 2)) min (screen_bounds.width * bounds).toInt
- val h =
- (font_metrics.getHeight * (lines + 2)) min (screen_bounds.height * bounds).toInt
+ val w = (Pretty.char_width_int(fm) * (margin + 2)) min (screen_bounds.width * bounds).toInt
+ val h = (fm.getHeight * (lines + 2)) min (screen_bounds.height * bounds).toInt
pretty_text_area.setPreferredSize(new Dimension(w, h))
window.pack
--- a/src/Tools/jEdit/src/rich_text_area.scala Sat Jan 12 16:49:40 2013 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Sat Jan 12 20:42:20 2013 +0100
@@ -490,7 +490,7 @@
val offset = caret - text_area.getLineStartOffset(physical_line)
val x = text_area.offsetToXY(physical_line, offset).x
gfx.setColor(painter.getCaretColor)
- gfx.drawRect(x, y, JEdit_Lib.char_width(text_area) - 1, fm.getHeight - 1)
+ gfx.drawRect(x, y, Pretty.char_width_int(fm) - 1, fm.getHeight - 1)
}
}
}