1.1 --- a/src/Pure/General/markup.ML Wed Sep 08 13:30:41 2010 +0100
1.2 +++ b/src/Pure/General/markup.ML Wed Sep 08 14:46:21 2010 +0200
1.3 @@ -58,6 +58,7 @@
1.4 val literalN: string val literal: T
1.5 val inner_stringN: string val inner_string: T
1.6 val inner_commentN: string val inner_comment: T
1.7 + val token_rangeN: string val token_range: T
1.8 val sortN: string val sort: T
1.9 val typN: string val typ: T
1.10 val termN: string val term: T
1.11 @@ -119,6 +120,7 @@
1.12 val promptN: string val prompt: T
1.13 val readyN: string val ready: T
1.14 val reportN: string val report: T
1.15 + val badN: string val bad: T
1.16 val no_output: output * output
1.17 val default_output: T -> output * output
1.18 val add_mode: string -> (T -> output * output) -> unit
1.19 @@ -239,6 +241,8 @@
1.20 val (inner_stringN, inner_string) = markup_elem "inner_string";
1.21 val (inner_commentN, inner_comment) = markup_elem "inner_comment";
1.22
1.23 +val (token_rangeN, token_range) = markup_elem "token_range";
1.24 +
1.25 val (sortN, sort) = markup_elem "sort";
1.26 val (typN, typ) = markup_elem "typ";
1.27 val (termN, term) = markup_elem "term";
1.28 @@ -345,6 +349,8 @@
1.29
1.30 val (reportN, report) = markup_elem "report";
1.31
1.32 +val (badN, bad) = markup_elem "bad";
1.33 +
1.34
1.35
1.36 (** print mode operations **)
2.1 --- a/src/Pure/General/markup.scala Wed Sep 08 13:30:41 2010 +0100
2.2 +++ b/src/Pure/General/markup.scala Wed Sep 08 14:46:21 2010 +0200
2.3 @@ -136,6 +136,8 @@
2.4 val LITERAL = "literal"
2.5 val INNER_COMMENT = "inner_comment"
2.6
2.7 + val TOKEN_RANGE = "token_range"
2.8 +
2.9 val SORT = "sort"
2.10 val TYP = "typ"
2.11 val TERM = "term"
2.12 @@ -247,6 +249,8 @@
2.13 val SIGNAL = "signal"
2.14 val EXIT = "exit"
2.15
2.16 + val BAD = "bad"
2.17 +
2.18 val Ready = Markup("ready", Nil)
2.19
2.20
3.1 --- a/src/Pure/Isar/proof_context.ML Wed Sep 08 13:30:41 2010 +0100
3.2 +++ b/src/Pure/Isar/proof_context.ML Wed Sep 08 14:46:21 2010 +0200
3.3 @@ -736,18 +736,22 @@
3.4
3.5 local
3.6
3.7 +fun parse_failed ctxt pos msg kind =
3.8 + (Context_Position.report ctxt Markup.bad pos;
3.9 + cat_error msg ("Failed to parse " ^ kind));
3.10 +
3.11 fun parse_sort ctxt text =
3.12 let
3.13 val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
3.14 val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos)
3.15 - handle ERROR msg => cat_error msg "Failed to parse sort";
3.16 + handle ERROR msg => parse_failed ctxt pos msg "sort";
3.17 in Type.minimize_sort (tsig_of ctxt) S end;
3.18
3.19 fun parse_typ ctxt text =
3.20 let
3.21 val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
3.22 val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) (get_sort ctxt) (syms, pos)
3.23 - handle ERROR msg => cat_error msg "Failed to parse type";
3.24 + handle ERROR msg => parse_failed ctxt pos msg "type";
3.25 in T end;
3.26
3.27 fun parse_term T ctxt text =
3.28 @@ -764,7 +768,7 @@
3.29 val t =
3.30 Syntax.standard_parse_term check get_sort map_const map_free
3.31 ctxt (Type.is_logtype (tsig_of ctxt)) (syn_of ctxt) T' (syms, pos)
3.32 - handle ERROR msg => cat_error msg ("Failed to parse " ^ kind);
3.33 + handle ERROR msg => parse_failed ctxt pos msg kind;
3.34 in t end;
3.35
3.36
4.1 --- a/src/Pure/PIDE/command.scala Wed Sep 08 13:30:41 2010 +0100
4.2 +++ b/src/Pure/PIDE/command.scala Wed Sep 08 14:46:21 2010 +0200
4.3 @@ -48,11 +48,11 @@
4.4 case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
4.5 (this /: msgs)((state, msg) =>
4.6 msg match {
4.7 - case XML.Elem(Markup(name, atts @ Position.Id_Range(id, range)), args)
4.8 - if id == command.id =>
4.9 + case XML.Elem(Markup(name, atts @ Position.Id_Range(id, raw_range)), args)
4.10 + if id == command.id && command.range.contains(command.decode(raw_range)) =>
4.11 + val range = command.decode(raw_range)
4.12 val props = Position.purge(atts)
4.13 - val info =
4.14 - Text.Info[Any](command.decode(range), XML.Elem(Markup(name, props), args))
4.15 + val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
4.16 state.add_markup(info)
4.17 case _ => System.err.println("Ignored report message: " + msg); state
4.18 })
4.19 @@ -60,8 +60,8 @@
4.20 atts match {
4.21 case Markup.Serial(i) =>
4.22 val result = XML.Elem(Markup(name, Position.purge(atts)), body)
4.23 - (add_result(i, result) /: Isar_Document.reported_positions(command.id, message))(
4.24 - (st, range) => st.add_markup(Text.Info(command.decode(range), result)))
4.25 + (add_result(i, result) /: Isar_Document.reported_positions(command, message))(
4.26 + (st, range) => st.add_markup(Text.Info(range, result)))
4.27 case _ => System.err.println("Ignored message without serial number: " + message); this
4.28 }
4.29 }
5.1 --- a/src/Pure/PIDE/document.scala Wed Sep 08 13:30:41 2010 +0100
5.2 +++ b/src/Pure/PIDE/document.scala Wed Sep 08 14:46:21 2010 +0200
5.3 @@ -169,11 +169,11 @@
5.4 def lookup_command(id: Command_ID): Option[Command]
5.5 def state(command: Command): Command.State
5.6 def convert(i: Text.Offset): Text.Offset
5.7 - def convert(range: Text.Range): Text.Range = range.map(convert(_))
5.8 + def convert(range: Text.Range): Text.Range
5.9 def revert(i: Text.Offset): Text.Offset
5.10 - def revert(range: Text.Range): Text.Range = range.map(revert(_))
5.11 - def select_markup[A](range: Text.Range)
5.12 - (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]]
5.13 + def revert(range: Text.Range): Text.Range
5.14 + def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
5.15 + : Stream[Text.Info[Option[A]]]
5.16 }
5.17
5.18 object State
5.19 @@ -304,18 +304,24 @@
5.20 def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
5.21 def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
5.22
5.23 - def select_markup[A](range: Text.Range)
5.24 - (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] =
5.25 + def convert(range: Text.Range): Text.Range =
5.26 + if (edits.isEmpty) range else range.map(convert(_))
5.27 +
5.28 + def revert(range: Text.Range): Text.Range =
5.29 + if (edits.isEmpty) range else range.map(revert(_))
5.30 +
5.31 + def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
5.32 + : Stream[Text.Info[Option[A]]] =
5.33 {
5.34 val former_range = revert(range)
5.35 for {
5.36 - (command, command_start) <- node.command_range(former_range)
5.37 + (command, command_start) <- node.command_range(former_range).toStream
5.38 Text.Info(r0, x) <- state(command).markup.
5.39 select((former_range - command_start).restrict(command.range)) {
5.40 case Text.Info(r0, info)
5.41 if result.isDefinedAt(Text.Info(convert(r0 + command_start), info)) =>
5.42 result(Text.Info(convert(r0 + command_start), info))
5.43 - } { default }
5.44 + }
5.45 val r = convert(r0 + command_start)
5.46 if !r.is_singularity
5.47 } yield Text.Info(r, x)
6.1 --- a/src/Pure/PIDE/isar_document.scala Wed Sep 08 13:30:41 2010 +0100
6.2 +++ b/src/Pure/PIDE/isar_document.scala Wed Sep 08 14:46:21 2010 +0200
6.3 @@ -61,19 +61,27 @@
6.4 private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
6.5 private val exclude_pos = Set(Markup.LOCATION)
6.6
6.7 - def reported_positions(command_id: Document.Command_ID, message: XML.Elem): Set[Text.Range] =
6.8 + private def is_state(msg: XML.Tree): Boolean =
6.9 + msg match {
6.10 + case XML.Elem(Markup(Markup.WRITELN, _), List(XML.Elem(Markup(Markup.STATE, _), _))) => true
6.11 + case _ => false
6.12 + }
6.13 +
6.14 + def reported_positions(command: Command, message: XML.Elem): Set[Text.Range] =
6.15 {
6.16 def reported(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
6.17 tree match {
6.18 - case XML.Elem(Markup(name, Position.Id_Range(id, range)), body)
6.19 - if include_pos(name) && id == command_id =>
6.20 - body.foldLeft(set + range)(reported)
6.21 + case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
6.22 + if include_pos(name) && id == command.id =>
6.23 + val range = command.decode(raw_range).restrict(command.range)
6.24 + body.foldLeft(if (range.is_singularity) set else set + range)(reported)
6.25 case XML.Elem(Markup(name, _), body) if !exclude_pos(name) =>
6.26 body.foldLeft(set)(reported)
6.27 case _ => set
6.28 }
6.29 val set = reported(Set.empty, message)
6.30 - if (set.isEmpty) set ++ Position.Range.unapply(message.markup.properties)
6.31 + if (set.isEmpty && !is_state(message))
6.32 + set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))
6.33 else set
6.34 }
6.35 }
7.1 --- a/src/Pure/PIDE/markup_tree.scala Wed Sep 08 13:30:41 2010 +0100
7.2 +++ b/src/Pure/PIDE/markup_tree.scala Wed Sep 08 14:46:21 2010 +0200
7.3 @@ -43,6 +43,8 @@
7.4 }
7.5
7.6 val empty = new Markup_Tree(Branches.empty)
7.7 +
7.8 + type Select[A] = PartialFunction[Text.Info[Any], A]
7.9 }
7.10
7.11
7.12 @@ -89,11 +91,13 @@
7.13 private def overlapping(range: Text.Range): Stream[(Text.Range, Branches.Entry)] =
7.14 Branches.overlapping(range, branches).toStream
7.15
7.16 - def select[A](root_range: Text.Range)
7.17 - (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] =
7.18 + def select[A](root_range: Text.Range)(result: Markup_Tree.Select[A])
7.19 + : Stream[Text.Info[Option[A]]] =
7.20 {
7.21 - def stream(last: Text.Offset, stack: List[(Text.Info[A], Stream[(Text.Range, Branches.Entry)])])
7.22 - : Stream[Text.Info[A]] =
7.23 + def stream(
7.24 + last: Text.Offset,
7.25 + stack: List[(Text.Info[Option[A]], Stream[(Text.Range, Branches.Entry)])])
7.26 + : Stream[Text.Info[Option[A]]] =
7.27 {
7.28 stack match {
7.29 case (parent, (range, (info, tree)) #:: more) :: rest =>
7.30 @@ -102,7 +106,7 @@
7.31 val start = subrange.start
7.32
7.33 if (result.isDefinedAt(info)) {
7.34 - val next = Text.Info(subrange, result(info))
7.35 + val next = Text.Info[Option[A]](subrange, Some(result(info)))
7.36 val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
7.37 if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts
7.38 else nexts
7.39 @@ -117,12 +121,11 @@
7.40
7.41 case Nil =>
7.42 val stop = root_range.stop
7.43 - if (last < stop) Stream(Text.Info(Text.Range(last, stop), default))
7.44 + if (last < stop) Stream(Text.Info(Text.Range(last, stop), None))
7.45 else Stream.empty
7.46 }
7.47 }
7.48 - stream(root_range.start, List((Text.Info(root_range, default), overlapping(root_range))))
7.49 - .iterator
7.50 + stream(root_range.start, List((Text.Info(root_range, None), overlapping(root_range))))
7.51 }
7.52
7.53 def swing_tree(parent: DefaultMutableTreeNode)
8.1 --- a/src/Pure/Syntax/lexicon.ML Wed Sep 08 13:30:41 2010 +0100
8.2 +++ b/src/Pure/Syntax/lexicon.ML Wed Sep 08 14:46:21 2010 +0200
8.3 @@ -66,6 +66,7 @@
8.4 val terminals: string list
8.5 val is_terminal: string -> bool
8.6 val report_token: Proof.context -> token -> unit
8.7 + val report_token_range: Proof.context -> token -> unit
8.8 val matching_tokens: token * token -> bool
8.9 val valued_token: token -> bool
8.10 val predef_term: string -> token option
8.11 @@ -188,6 +189,11 @@
8.12 fun report_token ctxt (Token (kind, _, (pos, _))) =
8.13 Context_Position.report ctxt (token_kind_markup kind) pos;
8.14
8.15 +fun report_token_range ctxt tok =
8.16 + if is_proper tok
8.17 + then Context_Position.report ctxt Markup.token_range (pos_of_token tok)
8.18 + else ();
8.19 +
8.20
8.21 (* matching_tokens *)
8.22
9.1 --- a/src/Pure/Syntax/syntax.ML Wed Sep 08 13:30:41 2010 +0100
9.2 +++ b/src/Pure/Syntax/syntax.ML Wed Sep 08 14:46:21 2010 +0200
9.3 @@ -709,7 +709,8 @@
9.4 val _ = List.app (Lexicon.report_token ctxt) toks;
9.5
9.6 val root' = if root <> "prop" andalso is_logtype root then Syn_Ext.logic else root;
9.7 - val pts = Parser.parse ctxt gram root' (filter Lexicon.is_proper toks);
9.8 + val pts = Parser.parse ctxt gram root' (filter Lexicon.is_proper toks)
9.9 + handle ERROR msg => (List.app (Lexicon.report_token_range ctxt) toks; error msg);
9.10 val len = length pts;
9.11
9.12 val limit = Config.get ctxt ambiguity_limit;
10.1 --- a/src/Tools/jEdit/dist-template/properties/jedit.props Wed Sep 08 13:30:41 2010 +0100
10.2 +++ b/src/Tools/jEdit/dist-template/properties/jedit.props Wed Sep 08 14:46:21 2010 +0200
10.3 @@ -177,6 +177,7 @@
10.4 end.shortcut=
10.5 fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
10.6 firstTime=false
10.7 +foldPainter=Circle
10.8 home.shortcut=
10.9 insert-newline-indent.shortcut=
10.10 insert-newline.shortcut=ENTER
10.11 @@ -203,6 +204,7 @@
10.12 view.fontsize=18
10.13 view.fracFontMetrics=false
10.14 view.gutter.fontsize=12
10.15 +view.gutter.selectionAreaWidth=18
10.16 view.height=787
10.17 view.middleMousePaste=true
10.18 view.showToolbar=false
11.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala Wed Sep 08 13:30:41 2010 +0100
11.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala Wed Sep 08 14:46:21 2010 +0200
11.3 @@ -69,87 +69,6 @@
11.4 case _ => false
11.5 }
11.6 }
11.7 -
11.8 -
11.9 - /* mapping to jEdit token types */
11.10 - // TODO: as properties or CSS style sheet
11.11 -
11.12 - val command_style: Map[String, Byte] =
11.13 - {
11.14 - import Token._
11.15 - Map[String, Byte](
11.16 - Keyword.THY_END -> KEYWORD2,
11.17 - Keyword.THY_SCRIPT -> LABEL,
11.18 - Keyword.PRF_SCRIPT -> LABEL,
11.19 - Keyword.PRF_ASM -> KEYWORD3,
11.20 - Keyword.PRF_ASM_GOAL -> KEYWORD3
11.21 - ).withDefaultValue(KEYWORD1)
11.22 - }
11.23 -
11.24 - val token_style: Map[String, Byte] =
11.25 - {
11.26 - import Token._
11.27 - Map[String, Byte](
11.28 - // logical entities
11.29 - Markup.TCLASS -> NULL,
11.30 - Markup.TYCON -> NULL,
11.31 - Markup.FIXED_DECL -> FUNCTION,
11.32 - Markup.FIXED -> NULL,
11.33 - Markup.CONST_DECL -> FUNCTION,
11.34 - Markup.CONST -> NULL,
11.35 - Markup.FACT_DECL -> FUNCTION,
11.36 - Markup.FACT -> NULL,
11.37 - Markup.DYNAMIC_FACT -> LABEL,
11.38 - Markup.LOCAL_FACT_DECL -> FUNCTION,
11.39 - Markup.LOCAL_FACT -> NULL,
11.40 - // inner syntax
11.41 - Markup.TFREE -> NULL,
11.42 - Markup.FREE -> NULL,
11.43 - Markup.TVAR -> NULL,
11.44 - Markup.SKOLEM -> NULL,
11.45 - Markup.BOUND -> NULL,
11.46 - Markup.VAR -> NULL,
11.47 - Markup.NUM -> DIGIT,
11.48 - Markup.FLOAT -> DIGIT,
11.49 - Markup.XNUM -> DIGIT,
11.50 - Markup.XSTR -> LITERAL4,
11.51 - Markup.LITERAL -> OPERATOR,
11.52 - Markup.INNER_COMMENT -> COMMENT1,
11.53 - Markup.SORT -> NULL,
11.54 - Markup.TYP -> NULL,
11.55 - Markup.TERM -> NULL,
11.56 - Markup.PROP -> NULL,
11.57 - Markup.ATTRIBUTE -> NULL,
11.58 - Markup.METHOD -> NULL,
11.59 - // ML syntax
11.60 - Markup.ML_KEYWORD -> KEYWORD1,
11.61 - Markup.ML_DELIMITER -> OPERATOR,
11.62 - Markup.ML_IDENT -> NULL,
11.63 - Markup.ML_TVAR -> NULL,
11.64 - Markup.ML_NUMERAL -> DIGIT,
11.65 - Markup.ML_CHAR -> LITERAL1,
11.66 - Markup.ML_STRING -> LITERAL1,
11.67 - Markup.ML_COMMENT -> COMMENT1,
11.68 - Markup.ML_MALFORMED -> INVALID,
11.69 - // embedded source text
11.70 - Markup.ML_SOURCE -> COMMENT3,
11.71 - Markup.DOC_SOURCE -> COMMENT3,
11.72 - Markup.ANTIQ -> COMMENT4,
11.73 - Markup.ML_ANTIQ -> COMMENT4,
11.74 - Markup.DOC_ANTIQ -> COMMENT4,
11.75 - // outer syntax
11.76 - Markup.KEYWORD -> KEYWORD2,
11.77 - Markup.OPERATOR -> OPERATOR,
11.78 - Markup.COMMAND -> KEYWORD1,
11.79 - Markup.IDENT -> NULL,
11.80 - Markup.VERBATIM -> COMMENT3,
11.81 - Markup.COMMENT -> COMMENT1,
11.82 - Markup.CONTROL -> COMMENT3,
11.83 - Markup.MALFORMED -> INVALID,
11.84 - Markup.STRING -> LITERAL3,
11.85 - Markup.ALTSTRING -> LITERAL1
11.86 - ).withDefaultValue(NULL)
11.87 - }
11.88 }
11.89
11.90
11.91 @@ -272,27 +191,18 @@
11.92 handler.handleToken(line_segment, style, offset, length, context)
11.93
11.94 val syntax = session.current_syntax()
11.95 - val token_markup: PartialFunction[Text.Info[Any], Byte] =
11.96 - {
11.97 - case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
11.98 - if syntax.keyword_kind(name).isDefined =>
11.99 - Document_Model.Token_Markup.command_style(syntax.keyword_kind(name).get)
11.100 -
11.101 - case Text.Info(_, XML.Elem(Markup(name, _), _))
11.102 - if Document_Model.Token_Markup.token_style(name) != Token.NULL =>
11.103 - Document_Model.Token_Markup.token_style(name)
11.104 - }
11.105 + val tokens = snapshot.select_markup(Text.Range(start, stop))(Isabelle_Markup.tokens(syntax))
11.106
11.107 var last = start
11.108 - for (token <- snapshot.select_markup(Text.Range(start, stop))(token_markup)(Token.NULL)) {
11.109 + for (token <- tokens.iterator) {
11.110 val Text.Range(token_start, token_stop) = token.range
11.111 if (last < token_start)
11.112 handle_token(Token.COMMENT1, last - start, token_start - last)
11.113 - handle_token(token.info, token_start - start, token_stop - token_start)
11.114 + handle_token(token.info getOrElse Token.NULL,
11.115 + token_start - start, token_stop - token_start)
11.116 last = token_stop
11.117 }
11.118 - if (last < stop)
11.119 - handle_token(Token.COMMENT1, last - start, stop - last)
11.120 + if (last < stop) handle_token(Token.COMMENT1, last - start, stop - last)
11.121
11.122 handle_token(Token.END, line_segment.count, 0)
11.123 handler.setLineContext(context)
12.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala Wed Sep 08 13:30:41 2010 +0100
12.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala Wed Sep 08 14:46:21 2010 +0200
12.3 @@ -13,42 +13,19 @@
12.4 import scala.actors.Actor._
12.5
12.6 import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent, FocusAdapter, FocusEvent}
12.7 -import java.awt.{BorderLayout, Graphics, Dimension, Color, Graphics2D}
12.8 +import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D}
12.9 import javax.swing.{JPanel, ToolTipManager}
12.10 import javax.swing.event.{CaretListener, CaretEvent}
12.11
12.12 -import org.gjt.sp.jedit.OperatingSystem
12.13 +import org.gjt.sp.jedit.{jEdit, OperatingSystem}
12.14 import org.gjt.sp.jedit.gui.RolloverButton
12.15 +import org.gjt.sp.jedit.options.GutterOptionPane
12.16 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
12.17 import org.gjt.sp.jedit.syntax.SyntaxStyle
12.18
12.19
12.20 object Document_View
12.21 {
12.22 - /* physical rendering */
12.23 -
12.24 - def status_color(snapshot: Document.Snapshot, command: Command): Color =
12.25 - {
12.26 - val state = snapshot.state(command)
12.27 - if (snapshot.is_outdated) new Color(240, 240, 240)
12.28 - else
12.29 - Isar_Document.command_status(state.status) match {
12.30 - case Isar_Document.Forked(i) if i > 0 => new Color(255, 228, 225)
12.31 - case Isar_Document.Finished => new Color(234, 248, 255)
12.32 - case Isar_Document.Failed => new Color(255, 193, 193)
12.33 - case Isar_Document.Unprocessed => new Color(255, 228, 225)
12.34 - case _ => Color.red
12.35 - }
12.36 - }
12.37 -
12.38 - val message_markup: PartialFunction[Text.Info[Any], Color] =
12.39 - {
12.40 - case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => new Color(220, 220, 220)
12.41 - case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => new Color(255, 165, 0)
12.42 - case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => new Color(255, 106, 106)
12.43 - }
12.44 -
12.45 -
12.46 /* document view of text area */
12.47
12.48 private val key = new Object
12.49 @@ -171,19 +148,17 @@
12.50
12.51 /* subexpression highlighting */
12.52
12.53 - private def subexp_range(snapshot: Document.Snapshot, x: Int, y: Int): Option[Text.Range] =
12.54 + private def subexp_range(snapshot: Document.Snapshot, x: Int, y: Int)
12.55 + : Option[(Text.Range, Color)] =
12.56 {
12.57 - val subexp_markup: PartialFunction[Text.Info[Any], Option[Text.Range]] =
12.58 - {
12.59 - case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), _)) =>
12.60 - Some(snapshot.convert(range))
12.61 + val offset = text_area.xyToOffset(x, y)
12.62 + snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.subexp) match {
12.63 + case Text.Info(_, Some((range, color))) #:: _ => Some((snapshot.convert(range), color))
12.64 + case _ => None
12.65 }
12.66 - val offset = text_area.xyToOffset(x, y)
12.67 - val markup = snapshot.select_markup(Text.Range(offset, offset + 1))(subexp_markup)(None)
12.68 - if (markup.hasNext) markup.next.info else None
12.69 }
12.70
12.71 - private var highlight_range: Option[Text.Range] = None
12.72 + private var highlight_range: Option[(Text.Range, Color)] = None
12.73
12.74 private val focus_listener = new FocusAdapter {
12.75 override def focusLost(e: FocusEvent) { highlight_range = None }
12.76 @@ -195,10 +170,10 @@
12.77 if (!model.buffer.isLoaded) highlight_range = None
12.78 else
12.79 Isabelle.swing_buffer_lock(model.buffer) {
12.80 - highlight_range.map(invalidate_line_range(_))
12.81 + highlight_range map { case (range, _) => invalidate_line_range(range) }
12.82 highlight_range =
12.83 if (control) subexp_range(model.snapshot(), e.getX(), e.getY()) else None
12.84 - highlight_range.map(invalidate_line_range(_))
12.85 + highlight_range map { case (range, _) => invalidate_line_range(range) }
12.86 }
12.87 }
12.88 }
12.89 @@ -217,53 +192,70 @@
12.90 val saved_color = gfx.getColor
12.91 val ascent = text_area.getPainter.getFontMetrics.getAscent
12.92
12.93 - try {
12.94 - for (i <- 0 until physical_lines.length) {
12.95 - if (physical_lines(i) != -1) {
12.96 - val line_range = proper_line_range(start(i), end(i))
12.97 + for (i <- 0 until physical_lines.length) {
12.98 + if (physical_lines(i) != -1) {
12.99 + val line_range = proper_line_range(start(i), end(i))
12.100
12.101 - // background color
12.102 - val cmds = snapshot.node.command_range(snapshot.revert(line_range))
12.103 - for {
12.104 - (command, command_start) <- cmds if !command.is_ignored
12.105 - val range = line_range.restrict(snapshot.convert(command.range + command_start))
12.106 - r <- Isabelle.gfx_range(text_area, range)
12.107 - } {
12.108 - gfx.setColor(Document_View.status_color(snapshot, command))
12.109 - gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
12.110 - }
12.111 + // background color: status
12.112 + val cmds = snapshot.node.command_range(snapshot.revert(line_range))
12.113 + for {
12.114 + (command, command_start) <- cmds if !command.is_ignored
12.115 + val range = line_range.restrict(snapshot.convert(command.range + command_start))
12.116 + r <- Isabelle.gfx_range(text_area, range)
12.117 + color <- Isabelle_Markup.status_color(snapshot, command)
12.118 + } {
12.119 + gfx.setColor(color)
12.120 + gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
12.121 + }
12.122
12.123 - // subexpression highlighting -- potentially from other snapshot
12.124 - if (highlight_range.isDefined) {
12.125 - if (line_range.overlaps(highlight_range.get)) {
12.126 - Isabelle.gfx_range(text_area, line_range.restrict(highlight_range.get)) match {
12.127 - case None =>
12.128 - case Some(r) =>
12.129 - gfx.setColor(Color.black)
12.130 - gfx.drawRect(r.x, y + i * line_height, r.length, line_height - 1)
12.131 - }
12.132 + // background color: markup
12.133 + for {
12.134 + Text.Info(range, Some(color)) <-
12.135 + snapshot.select_markup(line_range)(Isabelle_Markup.background).iterator
12.136 + r <- Isabelle.gfx_range(text_area, range)
12.137 + } {
12.138 + gfx.setColor(color)
12.139 + gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
12.140 + }
12.141 +
12.142 + // sub-expression highlighting -- potentially from other snapshot
12.143 + highlight_range match {
12.144 + case Some((range, color)) if line_range.overlaps(range) =>
12.145 + Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
12.146 + case None =>
12.147 + case Some(r) =>
12.148 + gfx.setColor(color)
12.149 + gfx.drawRect(r.x, y + i * line_height, r.length, line_height - 1)
12.150 }
12.151 - }
12.152 + case _ =>
12.153 + }
12.154
12.155 - // squiggly underline
12.156 - for {
12.157 - Text.Info(range, color) <-
12.158 - snapshot.select_markup(line_range)(Document_View.message_markup)(null)
12.159 - if color != null
12.160 - r <- Isabelle.gfx_range(text_area, range)
12.161 - } {
12.162 - gfx.setColor(color)
12.163 - val x0 = (r.x / 2) * 2
12.164 - val y0 = r.y + ascent + 1
12.165 - for (x1 <- Range(x0, x0 + r.length, 2)) {
12.166 - val y1 = if (x1 % 4 < 2) y0 else y0 + 1
12.167 - gfx.drawLine(x1, y1, x1 + 1, y1)
12.168 - }
12.169 + // boxed text
12.170 + for {
12.171 + Text.Info(range, Some(color)) <-
12.172 + snapshot.select_markup(line_range)(Isabelle_Markup.box).iterator
12.173 + r <- Isabelle.gfx_range(text_area, range)
12.174 + } {
12.175 + gfx.setColor(color)
12.176 + gfx.drawRect(r.x + 1, y + i * line_height + 1, r.length - 2, line_height - 3)
12.177 + }
12.178 +
12.179 + // squiggly underline
12.180 + for {
12.181 + Text.Info(range, Some(color)) <-
12.182 + snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
12.183 + r <- Isabelle.gfx_range(text_area, range)
12.184 + } {
12.185 + gfx.setColor(color)
12.186 + val x0 = (r.x / 2) * 2
12.187 + val y0 = r.y + ascent + 1
12.188 + for (x1 <- Range(x0, x0 + r.length, 2)) {
12.189 + val y1 = if (x1 % 4 < 2) y0 else y0 + 1
12.190 + gfx.drawLine(x1, y1, x1 + 1, y1)
12.191 }
12.192 }
12.193 }
12.194 }
12.195 - finally { gfx.setColor(saved_color) }
12.196 }
12.197 }
12.198
12.199 @@ -272,12 +264,52 @@
12.200 Isabelle.swing_buffer_lock(model.buffer) {
12.201 val snapshot = model.snapshot()
12.202 val offset = text_area.xyToOffset(x, y)
12.203 - val markup =
12.204 - snapshot.select_markup(Text.Range(offset, offset + 1)) {
12.205 - case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
12.206 - Isabelle.tooltip(Pretty.string_of(List(Pretty.block(body)), margin = 40))
12.207 - } { null }
12.208 - if (markup.hasNext) markup.next.info else null
12.209 + snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match
12.210 + {
12.211 + case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
12.212 + case _ => null
12.213 + }
12.214 + }
12.215 + }
12.216 + }
12.217 +
12.218 +
12.219 + /* gutter_extension */
12.220 +
12.221 + private val gutter_extension = new TextAreaExtension
12.222 + {
12.223 + override def paintScreenLineRange(gfx: Graphics2D,
12.224 + first_line: Int, last_line: Int, physical_lines: Array[Int],
12.225 + start: Array[Int], end: Array[Int], y: Int, line_height: Int)
12.226 + {
12.227 + val gutter = text_area.getGutter
12.228 + val width = GutterOptionPane.getSelectionAreaWidth
12.229 + val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
12.230 + val FOLD_MARKER_SIZE = 12
12.231 +
12.232 + if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
12.233 + Isabelle.swing_buffer_lock(model.buffer) {
12.234 + val snapshot = model.snapshot()
12.235 + for (i <- 0 until physical_lines.length) {
12.236 + if (physical_lines(i) != -1) {
12.237 + val line_range = proper_line_range(start(i), end(i))
12.238 +
12.239 + // gutter icons
12.240 + val icons =
12.241 + (for (Text.Info(_, Some(icon)) <-
12.242 + snapshot.select_markup(line_range)(Isabelle_Markup.gutter_message).iterator)
12.243 + yield icon).toList.sortWith(_ >= _)
12.244 + icons match {
12.245 + case icon :: _ =>
12.246 + val icn = icon.icon
12.247 + val x0 = (FOLD_MARKER_SIZE + width - border_width - icn.getIconWidth) max 10
12.248 + val y0 = y + i * line_height + (((line_height - icn.getIconHeight) / 2) max 0)
12.249 + icn.paintIcon(gutter, gfx, x0, y0)
12.250 + case Nil =>
12.251 + }
12.252 + }
12.253 + }
12.254 + }
12.255 }
12.256 }
12.257 }
12.258 @@ -328,13 +360,6 @@
12.259 super.removeNotify
12.260 }
12.261
12.262 - override def getToolTipText(event: MouseEvent): String =
12.263 - {
12.264 - val line = y_to_line(event.getY())
12.265 - if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>"
12.266 - else ""
12.267 - }
12.268 -
12.269 override def paintComponent(gfx: Graphics)
12.270 {
12.271 super.paintComponent(gfx)
12.272 @@ -342,18 +367,18 @@
12.273 val buffer = model.buffer
12.274 Isabelle.buffer_lock(buffer) {
12.275 val snapshot = model.snapshot()
12.276 - val saved_color = gfx.getColor // FIXME needed!?
12.277 - try {
12.278 - for ((command, start) <- snapshot.node.command_starts if !command.is_ignored) {
12.279 - val line1 = buffer.getLineOfOffset(snapshot.convert(start))
12.280 - val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
12.281 - val y = line_to_y(line1)
12.282 - val height = HEIGHT * (line2 - line1)
12.283 - gfx.setColor(Document_View.status_color(snapshot, command))
12.284 - gfx.fillRect(0, y, getWidth - 1, height)
12.285 - }
12.286 + for {
12.287 + (command, start) <- snapshot.node.command_starts
12.288 + if !command.is_ignored
12.289 + val line1 = buffer.getLineOfOffset(snapshot.convert(start))
12.290 + val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
12.291 + val y = line_to_y(line1)
12.292 + val height = HEIGHT * (line2 - line1)
12.293 + color <- Isabelle_Markup.overview_color(snapshot, command)
12.294 + } {
12.295 + gfx.setColor(color)
12.296 + gfx.fillRect(0, y, getWidth - 1, height)
12.297 }
12.298 - finally { gfx.setColor(saved_color) }
12.299 }
12.300 }
12.301
12.302 @@ -371,6 +396,7 @@
12.303 {
12.304 text_area.getPainter.
12.305 addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
12.306 + text_area.getGutter.addExtension(gutter_extension)
12.307 text_area.addFocusListener(focus_listener)
12.308 text_area.getPainter.addMouseMotionListener(mouse_motion_listener)
12.309 text_area.addCaretListener(caret_listener)
12.310 @@ -385,6 +411,7 @@
12.311 text_area.getPainter.removeMouseMotionListener(mouse_motion_listener)
12.312 text_area.removeCaretListener(caret_listener)
12.313 text_area.removeLeftOfScrollBar(overview)
12.314 + text_area.getGutter.removeExtension(gutter_extension)
12.315 text_area.getPainter.removeExtension(text_area_extension)
12.316 }
12.317 }
12.318 \ No newline at end of file
13.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Wed Sep 08 13:30:41 2010 +0100
13.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Wed Sep 08 14:46:21 2010 +0200
13.3 @@ -72,9 +72,11 @@
13.4 case _ => null
13.5 }
13.6 }
13.7 - } { null }
13.8 - if (markup.hasNext) markup.next.info else null
13.9 -
13.10 + }
13.11 + markup match {
13.12 + case Text.Info(_, Some(link)) #:: _ => link
13.13 + case _ => null
13.14 + }
13.15 case None => null
13.16 }
13.17 }
14.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
14.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala Wed Sep 08 14:46:21 2010 +0200
14.3 @@ -0,0 +1,198 @@
14.4 +/* Title: Tools/jEdit/src/jedit/isabelle_markup.scala
14.5 + Author: Makarius
14.6 +
14.7 +Isabelle specific physical rendering and markup selection.
14.8 +*/
14.9 +
14.10 +package isabelle.jedit
14.11 +
14.12 +
14.13 +import isabelle._
14.14 +
14.15 +import java.awt.Color
14.16 +
14.17 +import org.gjt.sp.jedit.GUIUtilities
14.18 +import org.gjt.sp.jedit.syntax.Token
14.19 +
14.20 +
14.21 +object Isabelle_Markup
14.22 +{
14.23 + /* physical rendering */
14.24 +
14.25 + val outdated_color = new Color(240, 240, 240)
14.26 + val unfinished_color = new Color(255, 228, 225)
14.27 +
14.28 + val regular_color = new Color(192, 192, 192)
14.29 + val warning_color = new Color(255, 168, 0)
14.30 + val error_color = new Color(255, 80, 80)
14.31 + val bad_color = new Color(255, 204, 153, 100)
14.32 +
14.33 + class Icon(val priority: Int, val icon: javax.swing.Icon)
14.34 + {
14.35 + def >= (that: Icon): Boolean = this.priority >= that.priority
14.36 + }
14.37 + val warning_icon = new Icon(1, GUIUtilities.loadIcon("16x16/status/dialog-warning.png"))
14.38 + val error_icon = new Icon(2, GUIUtilities.loadIcon("16x16/status/dialog-error.png"))
14.39 +
14.40 +
14.41 + /* command status */
14.42 +
14.43 + def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
14.44 + {
14.45 + val state = snapshot.state(command)
14.46 + if (snapshot.is_outdated) Some(outdated_color)
14.47 + else
14.48 + Isar_Document.command_status(state.status) match {
14.49 + case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
14.50 + case Isar_Document.Unprocessed => Some(unfinished_color)
14.51 + case _ => None
14.52 + }
14.53 + }
14.54 +
14.55 + def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
14.56 + {
14.57 + val state = snapshot.state(command)
14.58 + if (snapshot.is_outdated) None
14.59 + else
14.60 + Isar_Document.command_status(state.status) match {
14.61 + case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
14.62 + case Isar_Document.Unprocessed => Some(unfinished_color)
14.63 + case Isar_Document.Failed => Some(error_color)
14.64 + case _ => None
14.65 + }
14.66 + }
14.67 +
14.68 +
14.69 + /* markup selectors */
14.70 +
14.71 + private val subexp_include =
14.72 + Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING)
14.73 +
14.74 + val subexp: Markup_Tree.Select[(Text.Range, Color)] =
14.75 + {
14.76 + case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
14.77 + (range, Color.black)
14.78 + }
14.79 +
14.80 + val message: Markup_Tree.Select[Color] =
14.81 + {
14.82 + case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
14.83 + case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
14.84 + case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
14.85 + }
14.86 +
14.87 + val gutter_message: Markup_Tree.Select[Icon] =
14.88 + {
14.89 + case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_icon
14.90 + case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
14.91 + }
14.92 +
14.93 + val background: Markup_Tree.Select[Color] =
14.94 + {
14.95 + case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
14.96 + }
14.97 +
14.98 + val box: Markup_Tree.Select[Color] =
14.99 + {
14.100 + case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => regular_color
14.101 + }
14.102 +
14.103 + val tooltip: Markup_Tree.Select[String] =
14.104 + {
14.105 + case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
14.106 + Pretty.string_of(List(Pretty.block(body)), margin = 40)
14.107 + case Text.Info(_, XML.Elem(Markup(Markup.SORT, _), _)) => "sort"
14.108 + case Text.Info(_, XML.Elem(Markup(Markup.TYP, _), _)) => "type"
14.109 + case Text.Info(_, XML.Elem(Markup(Markup.TERM, _), _)) => "term"
14.110 + case Text.Info(_, XML.Elem(Markup(Markup.PROP, _), _)) => "proposition"
14.111 + }
14.112 +
14.113 +
14.114 + /* token markup -- text styles */
14.115 +
14.116 + private val command_style: Map[String, Byte] =
14.117 + {
14.118 + import Token._
14.119 + Map[String, Byte](
14.120 + Keyword.THY_END -> KEYWORD2,
14.121 + Keyword.THY_SCRIPT -> LABEL,
14.122 + Keyword.PRF_SCRIPT -> LABEL,
14.123 + Keyword.PRF_ASM -> KEYWORD3,
14.124 + Keyword.PRF_ASM_GOAL -> KEYWORD3
14.125 + ).withDefaultValue(KEYWORD1)
14.126 + }
14.127 +
14.128 + private val token_style: Map[String, Byte] =
14.129 + {
14.130 + import Token._
14.131 + Map[String, Byte](
14.132 + // logical entities
14.133 + Markup.TCLASS -> NULL,
14.134 + Markup.TYCON -> NULL,
14.135 + Markup.FIXED_DECL -> FUNCTION,
14.136 + Markup.FIXED -> NULL,
14.137 + Markup.CONST_DECL -> FUNCTION,
14.138 + Markup.CONST -> NULL,
14.139 + Markup.FACT_DECL -> FUNCTION,
14.140 + Markup.FACT -> NULL,
14.141 + Markup.DYNAMIC_FACT -> LABEL,
14.142 + Markup.LOCAL_FACT_DECL -> FUNCTION,
14.143 + Markup.LOCAL_FACT -> NULL,
14.144 + // inner syntax
14.145 + Markup.TFREE -> NULL,
14.146 + Markup.FREE -> NULL,
14.147 + Markup.TVAR -> NULL,
14.148 + Markup.SKOLEM -> NULL,
14.149 + Markup.BOUND -> NULL,
14.150 + Markup.VAR -> NULL,
14.151 + Markup.NUM -> DIGIT,
14.152 + Markup.FLOAT -> DIGIT,
14.153 + Markup.XNUM -> DIGIT,
14.154 + Markup.XSTR -> LITERAL4,
14.155 + Markup.LITERAL -> OPERATOR,
14.156 + Markup.INNER_COMMENT -> COMMENT1,
14.157 + Markup.SORT -> NULL,
14.158 + Markup.TYP -> NULL,
14.159 + Markup.TERM -> NULL,
14.160 + Markup.PROP -> NULL,
14.161 + Markup.ATTRIBUTE -> NULL,
14.162 + Markup.METHOD -> NULL,
14.163 + // ML syntax
14.164 + Markup.ML_KEYWORD -> KEYWORD1,
14.165 + Markup.ML_DELIMITER -> OPERATOR,
14.166 + Markup.ML_IDENT -> NULL,
14.167 + Markup.ML_TVAR -> NULL,
14.168 + Markup.ML_NUMERAL -> DIGIT,
14.169 + Markup.ML_CHAR -> LITERAL1,
14.170 + Markup.ML_STRING -> LITERAL1,
14.171 + Markup.ML_COMMENT -> COMMENT1,
14.172 + Markup.ML_MALFORMED -> INVALID,
14.173 + // embedded source text
14.174 + Markup.ML_SOURCE -> COMMENT3,
14.175 + Markup.DOC_SOURCE -> COMMENT3,
14.176 + Markup.ANTIQ -> COMMENT4,
14.177 + Markup.ML_ANTIQ -> COMMENT4,
14.178 + Markup.DOC_ANTIQ -> COMMENT4,
14.179 + // outer syntax
14.180 + Markup.KEYWORD -> KEYWORD2,
14.181 + Markup.OPERATOR -> OPERATOR,
14.182 + Markup.COMMAND -> KEYWORD1,
14.183 + Markup.IDENT -> NULL,
14.184 + Markup.VERBATIM -> COMMENT3,
14.185 + Markup.COMMENT -> COMMENT1,
14.186 + Markup.CONTROL -> COMMENT3,
14.187 + Markup.MALFORMED -> INVALID,
14.188 + Markup.STRING -> LITERAL3,
14.189 + Markup.ALTSTRING -> LITERAL1
14.190 + ).withDefaultValue(NULL)
14.191 + }
14.192 +
14.193 + def tokens(syntax: Outer_Syntax): Markup_Tree.Select[Byte] =
14.194 + {
14.195 + case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
14.196 + if syntax.keyword_kind(name).isDefined => command_style(syntax.keyword_kind(name).get)
14.197 +
14.198 + case Text.Info(_, XML.Elem(Markup(name, _), _))
14.199 + if token_style(name) != Token.NULL => token_style(name)
14.200 + }
14.201 +}
15.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala Wed Sep 08 13:30:41 2010 +0100
15.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala Wed Sep 08 14:46:21 2010 +0200
15.3 @@ -286,10 +286,9 @@
15.4 Isabelle.setup_tooltips()
15.5 }
15.6
15.7 - override def stop()
15.8 + override def stop() // FIXME fragile
15.9 {
15.10 Isabelle.session.stop() // FIXME dialog!?
15.11 Isabelle.session = null
15.12 - Isabelle.system = null
15.13 }
15.14 }