merged
authorhuffman
Sun Aug 21 21:18:59 2011 -0700 (2011-08-21)
changeset 443667ce460760f99
parent 44365 5daa55003649
parent 44364 78c43fb3adb0
child 44376 9c5cc8134cba
merged
     1.1 --- a/src/HOL/Predicate.thy	Sun Aug 21 12:22:31 2011 -0700
     1.2 +++ b/src/HOL/Predicate.thy	Sun Aug 21 21:18:59 2011 -0700
     1.3 @@ -25,7 +25,6 @@
     1.4  
     1.5  subsection {* Predicates as (complete) lattices *}
     1.6  
     1.7 -
     1.8  text {*
     1.9    Handy introduction and elimination rules for @{text "\<le>"}
    1.10    on unary and binary predicates
    1.11 @@ -423,14 +422,6 @@
    1.12    "(\<And>w. eval P w \<longleftrightarrow> eval Q w) \<Longrightarrow> P = Q"
    1.13    by (cases P, cases Q) (auto simp add: fun_eq_iff)
    1.14  
    1.15 -lemma eval_mem [simp]:
    1.16 -  "x \<in> eval P \<longleftrightarrow> eval P x"
    1.17 -  by (simp add: mem_def)
    1.18 -
    1.19 -lemma eq_mem [simp]:
    1.20 -  "x \<in> (op =) y \<longleftrightarrow> x = y"
    1.21 -  by (auto simp add: mem_def)
    1.22 -
    1.23  instantiation pred :: (type) complete_lattice
    1.24  begin
    1.25  
    1.26 @@ -798,11 +789,11 @@
    1.27    "map f P = P \<guillemotright>= (single o f)"
    1.28  
    1.29  lemma eval_map [simp]:
    1.30 -  "eval (map f P) = image f (eval P)"
    1.31 +  "eval (map f P) = (\<Squnion>x\<in>{x. eval P x}. (\<lambda>y. f x = y))"
    1.32    by (auto simp add: map_def)
    1.33  
    1.34  enriched_type map: map
    1.35 -  by (auto intro!: pred_eqI simp add: fun_eq_iff image_compose)
    1.36 +  by (rule ext, rule pred_eqI, auto)+
    1.37  
    1.38  
    1.39  subsubsection {* Implementation *}
    1.40 @@ -1040,6 +1031,14 @@
    1.41  end;
    1.42  *}
    1.43  
    1.44 +lemma eval_mem [simp]:
    1.45 +  "x \<in> eval P \<longleftrightarrow> eval P x"
    1.46 +  by (simp add: mem_def)
    1.47 +
    1.48 +lemma eq_mem [simp]:
    1.49 +  "x \<in> (op =) y \<longleftrightarrow> x = y"
    1.50 +  by (auto simp add: mem_def)
    1.51 +
    1.52  no_notation
    1.53    bot ("\<bottom>") and
    1.54    top ("\<top>") and
     2.1 --- a/src/HOL/Tools/Function/function_common.ML	Sun Aug 21 12:22:31 2011 -0700
     2.2 +++ b/src/HOL/Tools/Function/function_common.ML	Sun Aug 21 21:18:59 2011 -0700
     2.3 @@ -333,7 +333,7 @@
     2.4  
     2.5  
     2.6  local
     2.7 -  val option_parser = Parse.group "option"
     2.8 +  val option_parser = Parse.group (fn () => "option")
     2.9      ((Parse.reserved "sequential" >> K Sequential)
    2.10       || ((Parse.reserved "default" |-- Parse.term) >> Default)
    2.11       || (Parse.reserved "domintros" >> K DomIntros)
     3.1 --- a/src/Pure/Isar/args.ML	Sun Aug 21 12:22:31 2011 -0700
     3.2 +++ b/src/Pure/Isar/args.ML	Sun Aug 21 21:18:59 2011 -0700
     3.3 @@ -227,7 +227,7 @@
     3.4  fun parse_args is_symid =
     3.5    let
     3.6      val keyword_symid = token (Parse.keyword_with is_symid);
     3.7 -    fun atom blk = Parse.group "argument"
     3.8 +    fun atom blk = Parse.group (fn () => "argument")
     3.9        (ident || keyword_symid || string || alt_string || token Parse.float_number ||
    3.10          (if blk then token (Parse.$$$ ",") else Scan.fail));
    3.11  
     4.1 --- a/src/Pure/Isar/outer_syntax.ML	Sun Aug 21 12:22:31 2011 -0700
     4.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sun Aug 21 21:18:59 2011 -0700
     4.3 @@ -62,7 +62,9 @@
     4.4  local
     4.5  
     4.6  fun terminate false = Scan.succeed ()
     4.7 -  | terminate true = Parse.group "end of input" (Scan.option Parse.sync -- Parse.semicolon >> K ());
     4.8 +  | terminate true =
     4.9 +      Parse.group (fn () => "end of input")
    4.10 +        (Scan.option Parse.sync -- Parse.semicolon >> K ());
    4.11  
    4.12  fun body cmd (name, _) =
    4.13    (case cmd name of
     5.1 --- a/src/Pure/Isar/parse.ML	Sun Aug 21 12:22:31 2011 -0700
     5.2 +++ b/src/Pure/Isar/parse.ML	Sun Aug 21 21:18:59 2011 -0700
     5.3 @@ -8,7 +8,7 @@
     5.4  sig
     5.5    type 'a parser = Token.T list -> 'a * Token.T list
     5.6    type 'a context_parser = Context.generic * Token.T list -> 'a * (Context.generic * Token.T list)
     5.7 -  val group: string -> (Token.T list -> 'a) -> Token.T list -> 'a
     5.8 +  val group: (unit -> string) -> (Token.T list -> 'a) -> Token.T list -> 'a
     5.9    val !!! : (Token.T list -> 'a) -> Token.T list -> 'a
    5.10    val !!!! : (Token.T list -> 'a) -> Token.T list -> 'a
    5.11    val triple1: ('a * 'b) * 'c -> 'a * 'b * 'c
    5.12 @@ -114,17 +114,15 @@
    5.13  
    5.14  (* group atomic parsers (no cuts!) *)
    5.15  
    5.16 -fun fail_with s = Scan.fail_with
    5.17 -  (fn [] => (fn () => s ^ " expected (past end-of-file!)")
    5.18 +fun group s scan = scan || Scan.fail_with
    5.19 +  (fn [] => (fn () => s () ^ " expected (past end-of-file!)")
    5.20      | tok :: _ =>
    5.21          (fn () =>
    5.22            (case Token.text_of tok of
    5.23              (txt, "") =>
    5.24 -              s ^ " expected,\nbut " ^ txt ^ Token.pos_of tok ^ " was found"
    5.25 +              s () ^ " expected,\nbut " ^ txt ^ Token.pos_of tok ^ " was found"
    5.26            | (txt1, txt2) =>
    5.27 -              s ^ " expected,\nbut " ^ txt1 ^ Token.pos_of tok ^ " was found:\n" ^ txt2)));
    5.28 -
    5.29 -fun group s scan = scan || fail_with s;
    5.30 +              s () ^ " expected,\nbut " ^ txt1 ^ Token.pos_of tok ^ " was found:\n" ^ txt2)));
    5.31  
    5.32  
    5.33  (* cut *)
    5.34 @@ -170,7 +168,8 @@
    5.35  fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.source_of;
    5.36  
    5.37  fun kind k =
    5.38 -  group (Token.str_of_kind k) (RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of));
    5.39 +  group (fn () => Token.str_of_kind k)
    5.40 +    (RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of));
    5.41  
    5.42  val command = kind Token.Command;
    5.43  val keyword = kind Token.Keyword;
    5.44 @@ -192,10 +191,11 @@
    5.45  val keyword_ident_or_symbolic = keyword_with Token.ident_or_symbolic;
    5.46  
    5.47  fun $$$ x =
    5.48 -  group (Token.str_of_kind Token.Keyword ^ " " ^ quote x) (keyword_with (fn y => x = y));
    5.49 +  group (fn () => Token.str_of_kind Token.Keyword ^ " " ^ quote x)
    5.50 +    (keyword_with (fn y => x = y));
    5.51  
    5.52  fun reserved x =
    5.53 -  group ("reserved identifier " ^ quote x)
    5.54 +  group (fn () => "reserved identifier " ^ quote x)
    5.55      (RESET_VALUE (Scan.one (Token.ident_with (fn y => x = y)) >> Token.content_of));
    5.56  
    5.57  val semicolon = $$$ ";";
    5.58 @@ -208,7 +208,7 @@
    5.59  val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
    5.60  val real = float_number >> (the o Real.fromString) || int >> Real.fromInt;
    5.61  
    5.62 -val tag_name = group "tag name" (short_ident || string);
    5.63 +val tag_name = group (fn () => "tag name") (short_ident || string);
    5.64  val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);
    5.65  
    5.66  val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
    5.67 @@ -240,11 +240,17 @@
    5.68  
    5.69  (* names and text *)
    5.70  
    5.71 -val name = group "name declaration" (short_ident || sym_ident || string || number);
    5.72 +val name = group (fn () => "name declaration") (short_ident || sym_ident || string || number);
    5.73 +
    5.74  val binding = position name >> Binding.make;
    5.75 -val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
    5.76 -val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
    5.77 -val path = group "file name/path specification" name >> Path.explode;
    5.78 +
    5.79 +val xname = group (fn () => "name reference")
    5.80 +  (short_ident || long_ident || sym_ident || string || number);
    5.81 +
    5.82 +val text = group (fn () => "text")
    5.83 +  (short_ident || long_ident || sym_ident || string || number || verbatim);
    5.84 +
    5.85 +val path = group (fn () => "file name/path specification") name >> Path.explode;
    5.86  
    5.87  val liberal_name = keyword_ident_or_symbolic || xname;
    5.88  
    5.89 @@ -254,7 +260,7 @@
    5.90  
    5.91  (* sorts and arities *)
    5.92  
    5.93 -val sort = group "sort" (inner_syntax xname);
    5.94 +val sort = group (fn () => "sort") (inner_syntax xname);
    5.95  
    5.96  val arity = xname -- ($$$ "::" |-- !!!
    5.97    (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
    5.98 @@ -265,8 +271,9 @@
    5.99  
   5.100  (* types *)
   5.101  
   5.102 -val typ_group = group "type"
   5.103 -  (short_ident || long_ident || sym_ident || type_ident || type_var || string || number);
   5.104 +val typ_group =
   5.105 +  group (fn () => "type")
   5.106 +    (short_ident || long_ident || sym_ident || type_ident || type_var || string || number);
   5.107  
   5.108  val typ = inner_syntax typ_group;
   5.109  
   5.110 @@ -324,24 +331,24 @@
   5.111  
   5.112  (* embedded source text *)
   5.113  
   5.114 -val ML_source = source_position (group "ML source" text);
   5.115 -val doc_source = source_position (group "document source" text);
   5.116 +val ML_source = source_position (group (fn () => "ML source") text);
   5.117 +val doc_source = source_position (group (fn () => "document source") text);
   5.118  
   5.119  
   5.120  (* terms *)
   5.121  
   5.122  val tm = short_ident || long_ident || sym_ident || term_var || number || string;
   5.123  
   5.124 -val term_group = group "term" tm;
   5.125 -val prop_group = group "proposition" tm;
   5.126 +val term_group = group (fn () => "term") tm;
   5.127 +val prop_group = group (fn () => "proposition") tm;
   5.128  
   5.129  val term = inner_syntax term_group;
   5.130  val prop = inner_syntax prop_group;
   5.131  
   5.132 -val type_const = inner_syntax (group "type constructor" xname);
   5.133 -val const = inner_syntax (group "constant" xname);
   5.134 +val type_const = inner_syntax (group (fn () => "type constructor") xname);
   5.135 +val const = inner_syntax (group (fn () => "constant") xname);
   5.136  
   5.137 -val literal_fact = inner_syntax (group "literal fact" alt_string);
   5.138 +val literal_fact = inner_syntax (group (fn () => "literal fact") alt_string);
   5.139  
   5.140  
   5.141  (* patterns *)
     6.1 --- a/src/Pure/Isar/parse_spec.ML	Sun Aug 21 12:22:31 2011 -0700
     6.2 +++ b/src/Pure/Isar/parse_spec.ML	Sun Aug 21 21:18:59 2011 -0700
     6.3 @@ -136,7 +136,7 @@
     6.4      val expr0 = plus1_unless locale_keyword expr1;
     6.5    in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
     6.6  
     6.7 -val context_element = Parse.group "context element" loc_element;
     6.8 +val context_element = Parse.group (fn () => "context element") loc_element;
     6.9  
    6.10  end;
    6.11  
     7.1 --- a/src/Pure/Thy/thy_header.ML	Sun Aug 21 12:22:31 2011 -0700
     7.2 +++ b/src/Pure/Thy/thy_header.ML	Sun Aug 21 21:18:59 2011 -0700
     7.3 @@ -29,8 +29,8 @@
     7.4  
     7.5  (* header args *)
     7.6  
     7.7 -val file_name = Parse.group "file name" Parse.name;
     7.8 -val theory_name = Parse.group "theory name" Parse.name;
     7.9 +val file_name = Parse.group (fn () => "file name") Parse.name;
    7.10 +val theory_name = Parse.group (fn () => "theory name") Parse.name;
    7.11  
    7.12  val file =
    7.13    Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false ||
     8.1 --- a/src/Pure/Thy/thy_syntax.ML	Sun Aug 21 12:22:31 2011 -0700
     8.2 +++ b/src/Pure/Thy/thy_syntax.ML	Sun Aug 21 21:18:59 2011 -0700
     8.3 @@ -115,15 +115,15 @@
     8.4  
     8.5  local
     8.6  
     8.7 -val is_whitespace = Token.is_kind Token.Space orf Token.is_kind Token.Comment;
     8.8 +val whitespace = Scan.many (not o Token.is_proper);
     8.9 +val whitespace1 = Scan.many1 (not o Token.is_proper);
    8.10  
    8.11 -val body =
    8.12 -  Scan.unless (Scan.many is_whitespace -- Scan.ahead (Parse.command || Parse.eof)) Parse.not_eof;
    8.13 +val body = Scan.unless (whitespace -- Scan.ahead (Parse.command || Parse.eof)) Parse.not_eof;
    8.14  
    8.15  val span =
    8.16    Scan.ahead Parse.command -- Parse.not_eof -- Scan.repeat body
    8.17      >> (fn ((name, c), bs) => Span (Command name, c :: bs)) ||
    8.18 -  Scan.many1 is_whitespace >> (fn toks => Span (Ignored, toks)) ||
    8.19 +  whitespace1 >> (fn toks => Span (Ignored, toks)) ||
    8.20    Scan.repeat1 body >> (fn toks => Span (Malformed, toks));
    8.21  
    8.22  in
     9.1 --- a/src/Tools/jEdit/src/document_model.scala	Sun Aug 21 12:22:31 2011 -0700
     9.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sun Aug 21 21:18:59 2011 -0700
     9.3 @@ -139,13 +139,13 @@
     9.4    {
     9.5      buffer.addBufferListener(buffer_listener)
     9.6      pending_edits.init()
     9.7 -    buffer.propertiesChanged()
     9.8 +    Token_Markup.refresh_buffer(buffer)
     9.9    }
    9.10  
    9.11    private def deactivate()
    9.12    {
    9.13      pending_edits.flush()
    9.14      buffer.removeBufferListener(buffer_listener)
    9.15 -    buffer.propertiesChanged()
    9.16 +    Token_Markup.refresh_buffer(buffer)
    9.17    }
    9.18  }
    10.1 --- a/src/Tools/jEdit/src/token_markup.scala	Sun Aug 21 12:22:31 2011 -0700
    10.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Sun Aug 21 21:18:59 2011 -0700
    10.3 @@ -14,9 +14,10 @@
    10.4  import java.awt.geom.AffineTransform
    10.5  
    10.6  import org.gjt.sp.util.SyntaxUtilities
    10.7 -import org.gjt.sp.jedit.Mode
    10.8 +import org.gjt.sp.jedit.{jEdit, Mode}
    10.9  import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler,
   10.10    ParserRuleSet, ModeProvider, XModeHandler, SyntaxStyle}
   10.11 +import org.gjt.sp.jedit.buffer.JEditBuffer
   10.12  
   10.13  import javax.swing.text.Segment
   10.14  
   10.15 @@ -79,10 +80,14 @@
   10.16    private def bold_style(style: SyntaxStyle): SyntaxStyle =
   10.17      font_style(style, _.deriveFont(Font.BOLD))
   10.18  
   10.19 +  private def hidden_color: Color = new Color(255, 255, 255, 0)
   10.20 +
   10.21    class Style_Extender extends SyntaxUtilities.StyleExtender
   10.22    {
   10.23 -    if (Symbol.font_names.length > 2)
   10.24 -      error("Too many user symbol fonts (max 2 permitted): " + Symbol.font_names.mkString(", "))
   10.25 +    val max_user_fonts = 2
   10.26 +    if (Symbol.font_names.length > max_user_fonts)
   10.27 +      error("Too many user symbol fonts (max " + max_user_fonts + " permitted): " +
   10.28 +        Symbol.font_names.mkString(", "))
   10.29  
   10.30      override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
   10.31      {
   10.32 @@ -93,11 +98,13 @@
   10.33          new_styles(subscript(i.toByte)) = script_style(style, -1)
   10.34          new_styles(superscript(i.toByte)) = script_style(style, 1)
   10.35          new_styles(bold(i.toByte)) = bold_style(style)
   10.36 +        for (idx <- 0 until max_user_fonts)
   10.37 +          new_styles(user_font(idx, i.toByte)) = style
   10.38          for ((family, idx) <- Symbol.font_index)
   10.39            new_styles(user_font(idx, i.toByte)) = font_style(style, imitate_font(family, _))
   10.40        }
   10.41        new_styles(hidden) =
   10.42 -        new SyntaxStyle(Color.white, null,
   10.43 +        new SyntaxStyle(hidden_color, null,
   10.44            { val font = styles(0).getFont
   10.45              transform_font(new Font(font.getFamily, 0, 1),
   10.46                AffineTransform.getScaleInstance(1.0, font.getSize.toDouble)) })
   10.47 @@ -144,7 +151,7 @@
   10.48  
   10.49    private val isabelle_rules = new ParserRuleSet("isabelle", "MAIN")
   10.50  
   10.51 -  private class Line_Context(val context: Scan.Context)
   10.52 +  private class Line_Context(val context: Option[Scan.Context])
   10.53      extends TokenMarker.LineContext(isabelle_rules, null)
   10.54    {
   10.55      override def hashCode: Int = context.hashCode
   10.56 @@ -160,17 +167,17 @@
   10.57      override def markTokens(context: TokenMarker.LineContext,
   10.58          handler: TokenHandler, line: Segment): TokenMarker.LineContext =
   10.59      {
   10.60 +      val line_ctxt =
   10.61 +        context match {
   10.62 +          case c: Line_Context => c.context
   10.63 +          case _ => Some(Scan.Finished)
   10.64 +        }
   10.65        val context1 =
   10.66 -        if (Isabelle.session.is_ready) {
   10.67 +        if (line_ctxt.isDefined && Isabelle.session.is_ready) {
   10.68            val syntax = Isabelle.session.current_syntax()
   10.69      
   10.70 -          val ctxt =
   10.71 -            context match {
   10.72 -              case c: Line_Context => c.context
   10.73 -              case _ => Scan.Finished
   10.74 -            }
   10.75 -          val (tokens, ctxt1) = syntax.scan_context(line, ctxt)
   10.76 -          val context1 = new Line_Context(ctxt1)
   10.77 +          val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
   10.78 +          val context1 = new Line_Context(Some(ctxt1))
   10.79      
   10.80            val extended = extended_styles(line)
   10.81      
   10.82 @@ -196,7 +203,7 @@
   10.83            context1
   10.84          }
   10.85          else {
   10.86 -          val context1 = new Line_Context(Scan.Finished)
   10.87 +          val context1 = new Line_Context(None)
   10.88            handler.handleToken(line, JEditToken.NULL, 0, line.count, context1)
   10.89            handler.handleToken(line, JEditToken.END, line.count, 0, context1)
   10.90            context1
   10.91 @@ -210,12 +217,12 @@
   10.92  
   10.93    /* mode provider */
   10.94  
   10.95 +  private val isabelle_token_marker = new Token_Markup.Marker
   10.96 +
   10.97    class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider
   10.98    {
   10.99      for (mode <- orig_provider.getModes) addMode(mode)
  10.100  
  10.101 -    val isabelle_token_marker = new Token_Markup.Marker
  10.102 -
  10.103      override def loadMode(mode: Mode, xmh: XModeHandler)
  10.104      {
  10.105        super.loadMode(mode, xmh)
  10.106 @@ -223,5 +230,12 @@
  10.107          mode.setTokenMarker(isabelle_token_marker)
  10.108      }
  10.109    }
  10.110 +
  10.111 +  def refresh_buffer(buffer: JEditBuffer)
  10.112 +  {
  10.113 +    buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
  10.114 +    buffer.setTokenMarker(isabelle_token_marker)
  10.115 +    buffer.propertiesChanged
  10.116 +  }
  10.117  }
  10.118