1.1 --- a/src/HOL/Tools/Function/function_common.ML Sun Aug 21 11:03:15 2011 -0700
1.2 +++ b/src/HOL/Tools/Function/function_common.ML Sun Aug 21 22:04:01 2011 +0200
1.3 @@ -333,7 +333,7 @@
1.4
1.5
1.6 local
1.7 - val option_parser = Parse.group "option"
1.8 + val option_parser = Parse.group (fn () => "option")
1.9 ((Parse.reserved "sequential" >> K Sequential)
1.10 || ((Parse.reserved "default" |-- Parse.term) >> Default)
1.11 || (Parse.reserved "domintros" >> K DomIntros)
2.1 --- a/src/Pure/Isar/args.ML Sun Aug 21 11:03:15 2011 -0700
2.2 +++ b/src/Pure/Isar/args.ML Sun Aug 21 22:04:01 2011 +0200
2.3 @@ -227,7 +227,7 @@
2.4 fun parse_args is_symid =
2.5 let
2.6 val keyword_symid = token (Parse.keyword_with is_symid);
2.7 - fun atom blk = Parse.group "argument"
2.8 + fun atom blk = Parse.group (fn () => "argument")
2.9 (ident || keyword_symid || string || alt_string || token Parse.float_number ||
2.10 (if blk then token (Parse.$$$ ",") else Scan.fail));
2.11
3.1 --- a/src/Pure/Isar/outer_syntax.ML Sun Aug 21 11:03:15 2011 -0700
3.2 +++ b/src/Pure/Isar/outer_syntax.ML Sun Aug 21 22:04:01 2011 +0200
3.3 @@ -62,7 +62,9 @@
3.4 local
3.5
3.6 fun terminate false = Scan.succeed ()
3.7 - | terminate true = Parse.group "end of input" (Scan.option Parse.sync -- Parse.semicolon >> K ());
3.8 + | terminate true =
3.9 + Parse.group (fn () => "end of input")
3.10 + (Scan.option Parse.sync -- Parse.semicolon >> K ());
3.11
3.12 fun body cmd (name, _) =
3.13 (case cmd name of
4.1 --- a/src/Pure/Isar/parse.ML Sun Aug 21 11:03:15 2011 -0700
4.2 +++ b/src/Pure/Isar/parse.ML Sun Aug 21 22:04:01 2011 +0200
4.3 @@ -8,7 +8,7 @@
4.4 sig
4.5 type 'a parser = Token.T list -> 'a * Token.T list
4.6 type 'a context_parser = Context.generic * Token.T list -> 'a * (Context.generic * Token.T list)
4.7 - val group: string -> (Token.T list -> 'a) -> Token.T list -> 'a
4.8 + val group: (unit -> string) -> (Token.T list -> 'a) -> Token.T list -> 'a
4.9 val !!! : (Token.T list -> 'a) -> Token.T list -> 'a
4.10 val !!!! : (Token.T list -> 'a) -> Token.T list -> 'a
4.11 val triple1: ('a * 'b) * 'c -> 'a * 'b * 'c
4.12 @@ -114,17 +114,15 @@
4.13
4.14 (* group atomic parsers (no cuts!) *)
4.15
4.16 -fun fail_with s = Scan.fail_with
4.17 - (fn [] => (fn () => s ^ " expected (past end-of-file!)")
4.18 +fun group s scan = scan || Scan.fail_with
4.19 + (fn [] => (fn () => s () ^ " expected (past end-of-file!)")
4.20 | tok :: _ =>
4.21 (fn () =>
4.22 (case Token.text_of tok of
4.23 (txt, "") =>
4.24 - s ^ " expected,\nbut " ^ txt ^ Token.pos_of tok ^ " was found"
4.25 + s () ^ " expected,\nbut " ^ txt ^ Token.pos_of tok ^ " was found"
4.26 | (txt1, txt2) =>
4.27 - s ^ " expected,\nbut " ^ txt1 ^ Token.pos_of tok ^ " was found:\n" ^ txt2)));
4.28 -
4.29 -fun group s scan = scan || fail_with s;
4.30 + s () ^ " expected,\nbut " ^ txt1 ^ Token.pos_of tok ^ " was found:\n" ^ txt2)));
4.31
4.32
4.33 (* cut *)
4.34 @@ -170,7 +168,8 @@
4.35 fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.source_of;
4.36
4.37 fun kind k =
4.38 - group (Token.str_of_kind k) (RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of));
4.39 + group (fn () => Token.str_of_kind k)
4.40 + (RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of));
4.41
4.42 val command = kind Token.Command;
4.43 val keyword = kind Token.Keyword;
4.44 @@ -192,10 +191,11 @@
4.45 val keyword_ident_or_symbolic = keyword_with Token.ident_or_symbolic;
4.46
4.47 fun $$$ x =
4.48 - group (Token.str_of_kind Token.Keyword ^ " " ^ quote x) (keyword_with (fn y => x = y));
4.49 + group (fn () => Token.str_of_kind Token.Keyword ^ " " ^ quote x)
4.50 + (keyword_with (fn y => x = y));
4.51
4.52 fun reserved x =
4.53 - group ("reserved identifier " ^ quote x)
4.54 + group (fn () => "reserved identifier " ^ quote x)
4.55 (RESET_VALUE (Scan.one (Token.ident_with (fn y => x = y)) >> Token.content_of));
4.56
4.57 val semicolon = $$$ ";";
4.58 @@ -208,7 +208,7 @@
4.59 val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
4.60 val real = float_number >> (the o Real.fromString) || int >> Real.fromInt;
4.61
4.62 -val tag_name = group "tag name" (short_ident || string);
4.63 +val tag_name = group (fn () => "tag name") (short_ident || string);
4.64 val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);
4.65
4.66 val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
4.67 @@ -240,11 +240,17 @@
4.68
4.69 (* names and text *)
4.70
4.71 -val name = group "name declaration" (short_ident || sym_ident || string || number);
4.72 +val name = group (fn () => "name declaration") (short_ident || sym_ident || string || number);
4.73 +
4.74 val binding = position name >> Binding.make;
4.75 -val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
4.76 -val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
4.77 -val path = group "file name/path specification" name >> Path.explode;
4.78 +
4.79 +val xname = group (fn () => "name reference")
4.80 + (short_ident || long_ident || sym_ident || string || number);
4.81 +
4.82 +val text = group (fn () => "text")
4.83 + (short_ident || long_ident || sym_ident || string || number || verbatim);
4.84 +
4.85 +val path = group (fn () => "file name/path specification") name >> Path.explode;
4.86
4.87 val liberal_name = keyword_ident_or_symbolic || xname;
4.88
4.89 @@ -254,7 +260,7 @@
4.90
4.91 (* sorts and arities *)
4.92
4.93 -val sort = group "sort" (inner_syntax xname);
4.94 +val sort = group (fn () => "sort") (inner_syntax xname);
4.95
4.96 val arity = xname -- ($$$ "::" |-- !!!
4.97 (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
4.98 @@ -265,8 +271,9 @@
4.99
4.100 (* types *)
4.101
4.102 -val typ_group = group "type"
4.103 - (short_ident || long_ident || sym_ident || type_ident || type_var || string || number);
4.104 +val typ_group =
4.105 + group (fn () => "type")
4.106 + (short_ident || long_ident || sym_ident || type_ident || type_var || string || number);
4.107
4.108 val typ = inner_syntax typ_group;
4.109
4.110 @@ -324,24 +331,24 @@
4.111
4.112 (* embedded source text *)
4.113
4.114 -val ML_source = source_position (group "ML source" text);
4.115 -val doc_source = source_position (group "document source" text);
4.116 +val ML_source = source_position (group (fn () => "ML source") text);
4.117 +val doc_source = source_position (group (fn () => "document source") text);
4.118
4.119
4.120 (* terms *)
4.121
4.122 val tm = short_ident || long_ident || sym_ident || term_var || number || string;
4.123
4.124 -val term_group = group "term" tm;
4.125 -val prop_group = group "proposition" tm;
4.126 +val term_group = group (fn () => "term") tm;
4.127 +val prop_group = group (fn () => "proposition") tm;
4.128
4.129 val term = inner_syntax term_group;
4.130 val prop = inner_syntax prop_group;
4.131
4.132 -val type_const = inner_syntax (group "type constructor" xname);
4.133 -val const = inner_syntax (group "constant" xname);
4.134 +val type_const = inner_syntax (group (fn () => "type constructor") xname);
4.135 +val const = inner_syntax (group (fn () => "constant") xname);
4.136
4.137 -val literal_fact = inner_syntax (group "literal fact" alt_string);
4.138 +val literal_fact = inner_syntax (group (fn () => "literal fact") alt_string);
4.139
4.140
4.141 (* patterns *)
5.1 --- a/src/Pure/Isar/parse_spec.ML Sun Aug 21 11:03:15 2011 -0700
5.2 +++ b/src/Pure/Isar/parse_spec.ML Sun Aug 21 22:04:01 2011 +0200
5.3 @@ -136,7 +136,7 @@
5.4 val expr0 = plus1_unless locale_keyword expr1;
5.5 in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
5.6
5.7 -val context_element = Parse.group "context element" loc_element;
5.8 +val context_element = Parse.group (fn () => "context element") loc_element;
5.9
5.10 end;
5.11
6.1 --- a/src/Pure/Thy/thy_header.ML Sun Aug 21 11:03:15 2011 -0700
6.2 +++ b/src/Pure/Thy/thy_header.ML Sun Aug 21 22:04:01 2011 +0200
6.3 @@ -29,8 +29,8 @@
6.4
6.5 (* header args *)
6.6
6.7 -val file_name = Parse.group "file name" Parse.name;
6.8 -val theory_name = Parse.group "theory name" Parse.name;
6.9 +val file_name = Parse.group (fn () => "file name") Parse.name;
6.10 +val theory_name = Parse.group (fn () => "theory name") Parse.name;
6.11
6.12 val file =
6.13 Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false ||
7.1 --- a/src/Pure/Thy/thy_syntax.ML Sun Aug 21 11:03:15 2011 -0700
7.2 +++ b/src/Pure/Thy/thy_syntax.ML Sun Aug 21 22:04:01 2011 +0200
7.3 @@ -115,15 +115,15 @@
7.4
7.5 local
7.6
7.7 -val is_whitespace = Token.is_kind Token.Space orf Token.is_kind Token.Comment;
7.8 +val whitespace = Scan.many (not o Token.is_proper);
7.9 +val whitespace1 = Scan.many1 (not o Token.is_proper);
7.10
7.11 -val body =
7.12 - Scan.unless (Scan.many is_whitespace -- Scan.ahead (Parse.command || Parse.eof)) Parse.not_eof;
7.13 +val body = Scan.unless (whitespace -- Scan.ahead (Parse.command || Parse.eof)) Parse.not_eof;
7.14
7.15 val span =
7.16 Scan.ahead Parse.command -- Parse.not_eof -- Scan.repeat body
7.17 >> (fn ((name, c), bs) => Span (Command name, c :: bs)) ||
7.18 - Scan.many1 is_whitespace >> (fn toks => Span (Ignored, toks)) ||
7.19 + whitespace1 >> (fn toks => Span (Ignored, toks)) ||
7.20 Scan.repeat1 body >> (fn toks => Span (Malformed, toks));
7.21
7.22 in
8.1 --- a/src/Tools/jEdit/src/document_model.scala Sun Aug 21 11:03:15 2011 -0700
8.2 +++ b/src/Tools/jEdit/src/document_model.scala Sun Aug 21 22:04:01 2011 +0200
8.3 @@ -139,13 +139,13 @@
8.4 {
8.5 buffer.addBufferListener(buffer_listener)
8.6 pending_edits.init()
8.7 - buffer.propertiesChanged()
8.8 + Token_Markup.refresh_buffer(buffer)
8.9 }
8.10
8.11 private def deactivate()
8.12 {
8.13 pending_edits.flush()
8.14 buffer.removeBufferListener(buffer_listener)
8.15 - buffer.propertiesChanged()
8.16 + Token_Markup.refresh_buffer(buffer)
8.17 }
8.18 }
9.1 --- a/src/Tools/jEdit/src/token_markup.scala Sun Aug 21 11:03:15 2011 -0700
9.2 +++ b/src/Tools/jEdit/src/token_markup.scala Sun Aug 21 22:04:01 2011 +0200
9.3 @@ -14,9 +14,10 @@
9.4 import java.awt.geom.AffineTransform
9.5
9.6 import org.gjt.sp.util.SyntaxUtilities
9.7 -import org.gjt.sp.jedit.Mode
9.8 +import org.gjt.sp.jedit.{jEdit, Mode}
9.9 import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler,
9.10 ParserRuleSet, ModeProvider, XModeHandler, SyntaxStyle}
9.11 +import org.gjt.sp.jedit.buffer.JEditBuffer
9.12
9.13 import javax.swing.text.Segment
9.14
9.15 @@ -79,10 +80,14 @@
9.16 private def bold_style(style: SyntaxStyle): SyntaxStyle =
9.17 font_style(style, _.deriveFont(Font.BOLD))
9.18
9.19 + private def hidden_color: Color = new Color(255, 255, 255, 0)
9.20 +
9.21 class Style_Extender extends SyntaxUtilities.StyleExtender
9.22 {
9.23 - if (Symbol.font_names.length > 2)
9.24 - error("Too many user symbol fonts (max 2 permitted): " + Symbol.font_names.mkString(", "))
9.25 + val max_user_fonts = 2
9.26 + if (Symbol.font_names.length > max_user_fonts)
9.27 + error("Too many user symbol fonts (max " + max_user_fonts + " permitted): " +
9.28 + Symbol.font_names.mkString(", "))
9.29
9.30 override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
9.31 {
9.32 @@ -93,11 +98,13 @@
9.33 new_styles(subscript(i.toByte)) = script_style(style, -1)
9.34 new_styles(superscript(i.toByte)) = script_style(style, 1)
9.35 new_styles(bold(i.toByte)) = bold_style(style)
9.36 + for (idx <- 0 until max_user_fonts)
9.37 + new_styles(user_font(idx, i.toByte)) = style
9.38 for ((family, idx) <- Symbol.font_index)
9.39 new_styles(user_font(idx, i.toByte)) = font_style(style, imitate_font(family, _))
9.40 }
9.41 new_styles(hidden) =
9.42 - new SyntaxStyle(Color.white, null,
9.43 + new SyntaxStyle(hidden_color, null,
9.44 { val font = styles(0).getFont
9.45 transform_font(new Font(font.getFamily, 0, 1),
9.46 AffineTransform.getScaleInstance(1.0, font.getSize.toDouble)) })
9.47 @@ -144,7 +151,7 @@
9.48
9.49 private val isabelle_rules = new ParserRuleSet("isabelle", "MAIN")
9.50
9.51 - private class Line_Context(val context: Scan.Context)
9.52 + private class Line_Context(val context: Option[Scan.Context])
9.53 extends TokenMarker.LineContext(isabelle_rules, null)
9.54 {
9.55 override def hashCode: Int = context.hashCode
9.56 @@ -160,17 +167,17 @@
9.57 override def markTokens(context: TokenMarker.LineContext,
9.58 handler: TokenHandler, line: Segment): TokenMarker.LineContext =
9.59 {
9.60 + val line_ctxt =
9.61 + context match {
9.62 + case c: Line_Context => c.context
9.63 + case _ => Some(Scan.Finished)
9.64 + }
9.65 val context1 =
9.66 - if (Isabelle.session.is_ready) {
9.67 + if (line_ctxt.isDefined && Isabelle.session.is_ready) {
9.68 val syntax = Isabelle.session.current_syntax()
9.69
9.70 - val ctxt =
9.71 - context match {
9.72 - case c: Line_Context => c.context
9.73 - case _ => Scan.Finished
9.74 - }
9.75 - val (tokens, ctxt1) = syntax.scan_context(line, ctxt)
9.76 - val context1 = new Line_Context(ctxt1)
9.77 + val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
9.78 + val context1 = new Line_Context(Some(ctxt1))
9.79
9.80 val extended = extended_styles(line)
9.81
9.82 @@ -196,7 +203,7 @@
9.83 context1
9.84 }
9.85 else {
9.86 - val context1 = new Line_Context(Scan.Finished)
9.87 + val context1 = new Line_Context(None)
9.88 handler.handleToken(line, JEditToken.NULL, 0, line.count, context1)
9.89 handler.handleToken(line, JEditToken.END, line.count, 0, context1)
9.90 context1
9.91 @@ -210,12 +217,12 @@
9.92
9.93 /* mode provider */
9.94
9.95 + private val isabelle_token_marker = new Token_Markup.Marker
9.96 +
9.97 class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider
9.98 {
9.99 for (mode <- orig_provider.getModes) addMode(mode)
9.100
9.101 - val isabelle_token_marker = new Token_Markup.Marker
9.102 -
9.103 override def loadMode(mode: Mode, xmh: XModeHandler)
9.104 {
9.105 super.loadMode(mode, xmh)
9.106 @@ -223,5 +230,12 @@
9.107 mode.setTokenMarker(isabelle_token_marker)
9.108 }
9.109 }
9.110 +
9.111 + def refresh_buffer(buffer: JEditBuffer)
9.112 + {
9.113 + buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
9.114 + buffer.setTokenMarker(isabelle_token_marker)
9.115 + buffer.propertiesChanged
9.116 + }
9.117 }
9.118