# HG changeset patch
# User wenzelm
# Date 1418241393 -3600
# Node ID f4b6e2626cf80ce97a788b06e557df6d8f3bcfe4
# Parent  f65ac77f7e07f112f88292c7b44a36c8b735996d# Parent  6959ceb53ac855b87d2231291761feee95c5e11c
merged

diff -r f65ac77f7e07 -r f4b6e2626cf8 etc/isabelle.css
--- a/etc/isabelle.css	Tue Dec 09 16:22:40 2014 +0100
+++ b/etc/isabelle.css	Wed Dec 10 20:56:33 2014 +0100
@@ -3,13 +3,13 @@
 body { background-color: #FFFFFF; }
 
 .head     { background-color: #FFFFFF; }
-.source   { background-color: #F0F0F0; padding: 10px; }
+.source   { background-color: #FFFFFF; padding: 10px; }
 
-.external_source { background-color: #F0F0F0; padding: 10px; }
+.external_source { background-color: #FFFFFF; padding: 10px; }
 .external_footer { background-color: #FFFFFF; }
 
-.theories { background-color: #F0F0F0; padding: 10px; }
-.sessions { background-color: #F0F0F0; padding: 10px; }
+.theories { background-color: #FFFFFF; padding: 10px; }
+.sessions { background-color: #FFFFFF; padding: 10px; }
 
 .name     { font-style: italic; }
 .filename { font-family: fixed; }
@@ -29,23 +29,21 @@
 .numeral        { }
 .literal        { font-weight: bold; }
 .delimiter      { }
-.inner_string   { color: #D2691E; }
+.inner_string   { color: #FF00CC; }
 .inner_cartouche { color: #CC6600; }
-.inner_comment  { color: #8B0000; }
+.inner_comment  { color: #CC0000; }
 
 .bold           { font-weight: bold; }
 
-.keyword        { font-weight: bold; }
+.keyword1       { color: #006699; font-weight: bold; }
+.keyword2       { color: #009966; font-weight: bold; }
+.keyword3       { color: #0099FF; font-weight: bold; }
 .operator       { }
-.command        { font-weight: bold; }
-.string         { color: #008B00; }
-.altstring      { color: #8B8B00; }
-.verbatim       { color: #00008B; }
+.string         { color: #FF00CC; }
+.alt_string     { color: #CC00CC; }
+.verbatim       { color: #6600CC; }
 .cartouche      { color: #CC6600; }
-.comment        { color: #8B0000; }
-.control        { background-color: #FF6A6A; }
+.comment        { color: #CC0000; }
+.improper       { color: #FF5050; }
 .bad            { background-color: #FF6A6A; }
 
-.keyword1       { font-weight: bold; }
-.keyword2       { font-weight: bold; }
-
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Wed Dec 10 20:56:33 2014 +0100
@@ -468,8 +468,8 @@
 
   The @{antiquotation rail} antiquotation allows to include syntax
   diagrams into Isabelle documents.  {\LaTeX} requires the style file
-  @{file "~~/lib/texinputs/pdfsetup.sty"}, which can be used via
-  @{verbatim \<open>\usepackage{pdfsetup}\<close>} in @{verbatim "root.tex"}, for
+  @{file "~~/lib/texinputs/railsetup.sty"}, which can be used via
+  @{verbatim \<open>\usepackage{railsetup}\<close>} in @{verbatim "root.tex"}, for
   example.
 
   The rail specification language is quoted here as Isabelle @{syntax
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Wed Dec 10 20:56:33 2014 +0100
@@ -261,14 +261,27 @@
   by (\<open>rtac @{thm impI} 1\<close>, \<open>etac @{thm conjE} 1\<close>, \<open>rtac @{thm conjI} 1\<close>, \<open>atac 1\<close>+)
 
 
-subsection \<open>ML syntax: input source\<close>
+subsection \<open>ML syntax\<close>
 
+text \<open>Input source with position information:\<close>
 ML \<open>
   val s: Input.source = \<open>abc\<close>;
-  writeln ("Look here!" ^ Position.here (Input.pos_of s));
+  writeln (Markup.markup Markup.information ("Look here!" ^ Position.here (Input.pos_of s)));
 
   \<open>abc123def456\<close> |> Input.source_explode |> List.app (fn (s, pos) =>
     if Symbol.is_digit s then Position.report pos Markup.ML_numeral else ());
 \<close>
 
+text \<open>Nested ML evaluation:\<close>
+ML \<open>
+  val ML = ML_Context.eval_source ML_Compiler.flags;
+
+  ML \<open>ML \<open>val a = @{thm refl}\<close>\<close>;
+  ML \<open>val b = @{thm sym}\<close>;
+  val c = @{thm trans}
+  val thms = [a, b, c];
+\<close>
+
+ML \<open>\<close>
+
 end
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Provers/classical.ML	Wed Dec 10 20:56:33 2014 +0100
@@ -139,7 +139,7 @@
     [| inj f; f x = f y; x = y ==> PROP W |] ==> PROP W
 
 Such rules can cause fast_tac to fail and blast_tac to report "PROOF
-FAILED"; classical_rule will strenthen this to
+FAILED"; classical_rule will strengthen this to
 
     [| inj f; ~ W ==> f x = f y; x = y ==> W |] ==> W
 *)
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Pure/General/input.ML
--- a/src/Pure/General/input.ML	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Pure/General/input.ML	Wed Dec 10 20:56:33 2014 +0100
@@ -12,6 +12,7 @@
   val pos_of: source -> Position.T
   val range_of: source -> Position.range
   val source: bool -> Symbol_Pos.text -> Position.range -> source
+  val string: string -> source
   val source_explode: source -> Symbol_Pos.T list
   val source_content: source -> string
 end;
@@ -30,6 +31,8 @@
 fun source delimited text range =
   Source {delimited = delimited, text = text, range = range};
 
+fun string text = source true text Position.no_range;
+
 fun source_explode (Source {text, range = (pos, _), ...}) =
   Symbol_Pos.explode (text, pos);
 
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Pure/Isar/calculation.ML	Wed Dec 10 20:56:33 2014 +0100
@@ -111,7 +111,13 @@
 (** proof commands **)
 
 fun assert_sane final =
-  if final then Proof.assert_forward else Proof.assert_forward_or_chain;
+  if final then Proof.assert_forward
+  else
+    Proof.assert_forward_or_chain #>
+    tap (fn state =>
+      if can Proof.assert_chain state then
+        Context_Position.report (Proof.context_of state) (Position.thread_data ()) Markup.improper
+      else ());
 
 fun maintain_calculation int final calc state =
   let
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Pure/Isar/keyword.ML	Wed Dec 10 20:56:33 2014 +0100
@@ -41,6 +41,7 @@
   val is_keyword: keywords -> string -> bool
   val is_command: keywords -> string -> bool
   val is_literal: keywords -> string -> bool
+  val command_kind: keywords -> string -> string option
   val command_files: keywords -> string -> Path.T -> Path.T list
   val command_tags: keywords -> string -> string list
   val is_vacuous: keywords -> string -> bool
@@ -50,6 +51,7 @@
   val is_document_raw: keywords -> string -> bool
   val is_document: keywords -> string -> bool
   val is_theory_begin: keywords -> string -> bool
+  val is_theory_end: keywords -> string -> bool
   val is_theory_load: keywords -> string -> bool
   val is_theory: keywords -> string -> bool
   val is_theory_body: keywords -> string -> bool
@@ -59,6 +61,8 @@
   val is_proof_goal: keywords -> string -> bool
   val is_qed: keywords -> string -> bool
   val is_qed_global: keywords -> string -> bool
+  val is_proof_asm: keywords -> string -> bool
+  val is_improper: keywords -> string -> bool
   val is_printed: keywords -> string -> bool
 end;
 
@@ -177,10 +181,12 @@
 
 (* command kind *)
 
-fun command_kind (Keywords {commands, ...}) = Symtab.lookup commands;
+fun lookup_command (Keywords {commands, ...}) = Symtab.lookup commands;
+
+fun command_kind keywords = Option.map #kind o lookup_command keywords;
 
 fun command_files keywords name path =
-  (case command_kind keywords name of
+  (case lookup_command keywords name of
     NONE => []
   | SOME {kind, files, ...} =>
       if kind <> thy_load then []
@@ -188,7 +194,7 @@
       else map (fn ext => Path.ext ext path) files);
 
 fun command_tags keywords name =
-  (case command_kind keywords name of
+  (case lookup_command keywords name of
     SOME {tags, ...} => tags
   | NONE => []);
 
@@ -199,7 +205,7 @@
   let
     val tab = Symtab.make_set ks;
     fun pred keywords name =
-      (case command_kind keywords name of
+      (case lookup_command keywords name of
         NONE => false
       | SOME {kind, ...} => Symtab.defined tab kind);
   in pred end;
@@ -214,6 +220,7 @@
 val is_document = command_category [document_heading, document_body, document_raw];
 
 val is_theory_begin = command_category [thy_begin];
+val is_theory_end = command_category [thy_end];
 
 val is_theory_load = command_category [thy_load];
 
@@ -236,6 +243,9 @@
 val is_qed = command_category [qed, qed_script, qed_block];
 val is_qed_global = command_category [qed_global];
 
+val is_proof_asm = command_category [prf_asm, prf_asm_goal];
+val is_improper = command_category [qed_script, prf_script, prf_asm_goal_script];
+
 fun is_printed keywords = is_theory_goal keywords orf is_proof keywords;
 
 end;
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Pure/Isar/keyword.scala	Wed Dec 10 20:56:33 2014 +0100
@@ -139,10 +139,6 @@
 
     def command_kind(name: String): Option[String] = commands.get(name).map(_._1)
 
-    def is_command_kind(token: Token, pred: String => Boolean): Boolean =
-      token.is_command &&
-        (command_kind(token.source) match { case Some(k) => pred(k) case None => false })
-
 
     /* load commands */
 
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Wed Dec 10 20:56:33 2014 +0100
@@ -156,7 +156,7 @@
     val command1 = tokens.exists(_.is_command)
 
     val depth1 =
-      if (tokens.exists(tok => keywords.is_command_kind(tok, Keyword.theory))) 0
+      if (tokens.exists(tok => tok.is_command_kind(keywords, Keyword.theory))) 0
       else if (command1) struct.after_span_depth
       else struct.span_depth
 
@@ -164,15 +164,15 @@
       ((struct.span_depth, struct.after_span_depth) /: tokens) {
         case ((x, y), tok) =>
           if (tok.is_command) {
-            if (keywords.is_command_kind(tok, Keyword.theory_goal))
+            if (tok.is_command_kind(keywords, Keyword.theory_goal))
               (2, 1)
-            else if (keywords.is_command_kind(tok, Keyword.theory))
+            else if (tok.is_command_kind(keywords, Keyword.theory))
               (1, 0)
-            else if (keywords.is_command_kind(tok, Keyword.proof_goal) || tok.is_begin_block)
+            else if (tok.is_command_kind(keywords, Keyword.proof_goal) || tok.is_begin_block)
               (y + 2, y + 1)
-            else if (keywords.is_command_kind(tok, Keyword.qed) || tok.is_end_block)
+            else if (tok.is_command_kind(keywords, Keyword.qed) || tok.is_end_block)
               (y + 1, y - 1)
-            else if (keywords.is_command_kind(tok, Keyword.qed_global))
+            else if (tok.is_command_kind(keywords, Keyword.qed_global))
               (1, 0)
             else (x, y)
           }
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Pure/Isar/token.ML	Wed Dec 10 20:56:33 2014 +0100
@@ -60,8 +60,8 @@
   val content_of: T -> string
   val keyword_markup: bool * Markup.T -> string -> Markup.T
   val completion_report: T -> Position.report_text list
-  val report: T -> Position.report_text
-  val markup: T -> Markup.T
+  val reports: Keyword.keywords -> T -> Position.report_text list
+  val markups: Keyword.keywords -> T -> Markup.T list
   val unparse: T -> string
   val unparse_src: src -> string list
   val print: T -> string
@@ -233,6 +233,7 @@
 fun is_kind k (Token (_, (k', _), _)) = k = k';
 
 val is_command = is_kind Command;
+
 val is_name = is_kind Ident orf is_kind Sym_Ident orf is_kind String orf is_kind Nat;
 
 fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
@@ -293,25 +294,24 @@
 local
 
 val token_kind_markup =
- fn Command => (Markup.command, "")
-  | Keyword => (Markup.keyword2, "")
-  | Ident => (Markup.empty, "")
-  | Long_Ident => (Markup.empty, "")
-  | Sym_Ident => (Markup.empty, "")
-  | Var => (Markup.var, "")
+ fn Var => (Markup.var, "")
   | Type_Ident => (Markup.tfree, "")
   | Type_Var => (Markup.tvar, "")
-  | Nat => (Markup.empty, "")
-  | Float => (Markup.empty, "")
-  | Space => (Markup.empty, "")
   | String => (Markup.string, "")
   | Alt_String => (Markup.alt_string, "")
   | Verbatim => (Markup.verbatim, "")
   | Cartouche => (Markup.cartouche, "")
   | Comment => (Markup.comment, "")
   | Error msg => (Markup.bad, msg)
-  | Internal_Value => (Markup.empty, "")
-  | EOF => (Markup.empty, "");
+  | _ => (Markup.empty, "");
+
+fun keyword_reports tok = map (fn markup => ((pos_of tok, markup), ""));
+
+fun command_markups keywords x =
+  if Keyword.is_theory_end keywords x then [Markup.keyword2]
+  else if Keyword.is_proof_asm keywords x then [Markup.keyword3]
+  else if Keyword.is_improper keywords x then [Markup.keyword1, Markup.improper]
+  else [Markup.keyword1];
 
 in
 
@@ -323,14 +323,16 @@
   then map (fn m => ((pos_of tok, m), "")) (Completion.suppress_abbrevs (content_of tok))
   else [];
 
-fun report tok =
-  if is_kind Keyword tok then
-    ((pos_of tok, keyword_markup (false, Markup.keyword2) (content_of tok)), "")
+fun reports keywords tok =
+  if is_command tok then
+    keyword_reports tok (command_markups keywords (content_of tok))
+  else if is_kind Keyword tok then
+    keyword_reports tok [keyword_markup (false, Markup.keyword2) (content_of tok)]
   else
     let val (m, text) = token_kind_markup (kind_of tok)
-    in ((pos_of tok, m), text) end;
+    in [((pos_of tok, m), text)] end;
 
-val markup = #2 o #1 o report;
+fun markups keywords = map (#2 o #1) o reports keywords;
 
 end;
 
@@ -349,18 +351,18 @@
 
 fun unparse_src (Src {args, ...}) = map unparse args;
 
-fun print tok = Markup.markup (markup tok) (unparse tok);
+fun print tok = Markup.markups (markups Keyword.empty_keywords tok) (unparse tok);
 
 fun text_of tok =
   let
     val k = str_of_kind (kind_of tok);
-    val m = markup tok;
+    val ms = markups Keyword.empty_keywords tok;
     val s = unparse tok;
   in
     if s = "" then (k, "")
     else if size s < 40 andalso not (exists_string (fn c => c = "\n") s)
-    then (k ^ " " ^ Markup.markup m s, "")
-    else (k, Markup.markup m s)
+    then (k ^ " " ^ Markup.markups ms s, "")
+    else (k, Markup.markups ms s)
   end;
 
 
@@ -451,7 +453,7 @@
   | SOME (Term t) => Syntax.pretty_term ctxt t
   | SOME (Fact (_, ths)) =>
       Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.backquote o Display.pretty_thm ctxt) ths))
-  | _ => Pretty.mark_str (markup tok, unparse tok));
+  | _ => Pretty.marks_str (markups Keyword.empty_keywords tok, unparse tok));
 
 fun pretty_src ctxt src =
   let
@@ -464,6 +466,7 @@
   in Pretty.block (Pretty.breaks (prt_name :: map prt_arg args)) end;
 
 
+
 (** scanners **)
 
 open Basic_Symbol_Pos;
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Pure/Isar/token.scala	Wed Dec 10 20:56:33 2014 +0100
@@ -194,6 +194,9 @@
 sealed case class Token(val kind: Token.Kind.Value, val source: String)
 {
   def is_command: Boolean = kind == Token.Kind.COMMAND
+  def is_command_kind(keywords: Keyword.Keywords, pred: String => Boolean): Boolean =
+    is_command &&
+      (keywords.command_kind(source) match { case Some(k) => pred(k) case None => false })
   def is_keyword: Boolean = kind == Token.Kind.KEYWORD
   def is_delimiter: Boolean = is_keyword && !Symbol.is_ascii_identifier(source)
   def is_ident: Boolean = kind == Token.Kind.IDENT
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Pure/ML-Systems/ml_name_space.ML
--- a/src/Pure/ML-Systems/ml_name_space.ML	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Pure/ML-Systems/ml_name_space.ML	Wed Dec 10 20:56:33 2014 +0100
@@ -61,4 +61,6 @@
 val initial_signature : (string * signatureVal) list = [];
 val initial_functor : (string * functorVal) list = [];
 
+fun forget_global_structure (_: string) = ();
+
 end;
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Wed Dec 10 20:56:33 2014 +0100
@@ -19,6 +19,7 @@
   val initial_structure = #allStruct global ();
   val initial_signature = #allSig global ();
   val initial_functor = #allFunct global ();
+  val forget_global_structure = PolyML.Compiler.forgetStructure;
 end;
 
 
@@ -173,6 +174,7 @@
   use_text context (1, "pp") false
     ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
 
-val ml_make_string =
-  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, Isabelle.ML_print_depth ())))))";
+fun ml_make_string struct_name =
+  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, " ^
+    struct_name ^ ".ML_print_depth ())))))";
 
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Wed Dec 10 20:56:33 2014 +0100
@@ -65,7 +65,7 @@
   val _ = default_print_depth 10;
 end;
 
-val ml_make_string = "(fn _ => \"?\")";
+fun ml_make_string (_: string) = "(fn _ => \"?\")";
 
 
 (*prompts*)
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML	Wed Dec 10 20:56:33 2014 +0100
@@ -13,12 +13,14 @@
  (ML_Antiquotation.inline @{binding assert}
     (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
 
-  ML_Antiquotation.inline @{binding make_string} (Scan.succeed ml_make_string) #>
+  ML_Antiquotation.inline @{binding make_string}
+    (Args.context >> (ml_make_string o ML_Context.struct_name)) #>
 
   ML_Antiquotation.declaration @{binding print}
     (Scan.lift (Scan.optional Args.name "Output.writeln"))
       (fn src => fn output => fn ctxt =>
         let
+          val struct_name = ML_Context.struct_name ctxt;
           val (_, pos) = Token.name_of_src src;
           val (a, ctxt') = ML_Context.variant "output" ctxt;
           val env =
@@ -26,7 +28,7 @@
             \  (" ^ output ^ ") o (fn s => s ^ Position.here (" ^
             ML_Syntax.print_position pos ^ "));\n";
           val body =
-            "(fn x => (Isabelle." ^ a ^ " (" ^ ml_make_string ^ " x); x))";
+            "(fn x => (" ^ struct_name ^ "." ^ a ^ " (" ^ ml_make_string struct_name ^ " x); x))";
         in (K (env, body), ctxt') end));
 
 
@@ -52,7 +54,8 @@
        "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
         ML_Syntax.print_string name))) #>
 
-  ML_Antiquotation.inline @{binding context} (Scan.succeed "Isabelle.ML_context") #>
+  ML_Antiquotation.inline @{binding context}
+    (Args.context >> (fn ctxt => ML_Context.struct_name ctxt ^ ".ML_context")) #>
 
   ML_Antiquotation.inline @{binding typ} (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
   ML_Antiquotation.inline @{binding term} (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Pure/ML/ml_context.ML	Wed Dec 10 20:56:33 2014 +0100
@@ -13,14 +13,13 @@
   val thms: xstring -> thm list
   val exec: (unit -> unit) -> Context.generic -> Context.generic
   val check_antiquotation: Proof.context -> xstring * Position.T -> string
+  val struct_name: Proof.context -> string
   val variant: string -> Proof.context -> string * Proof.context
   type decl = Proof.context -> string * string
   val value_decl: string -> string -> Proof.context -> decl * Proof.context
   val add_antiquotation: binding -> (Token.src -> Proof.context -> decl * Proof.context) ->
     theory -> theory
   val print_antiquotations: Proof.context -> unit
-  val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
-    Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
   val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
   val eval_file: ML_Compiler.flags -> Path.T -> unit
   val eval_source: ML_Compiler.flags -> Input.source -> unit
@@ -52,20 +51,23 @@
 
 (** ML antiquotations **)
 
-(* unique names *)
+(* names for generated environment *)
 
 structure Names = Proof_Data
 (
-  type T = Name.context;
+  type T = string * Name.context;
   val init_names = ML_Syntax.reserved |> fold Name.declare ["ML_context", "ML_print_depth"];
-  fun init _ = init_names;
+  fun init _ = ("Isabelle0", init_names);
 );
 
+fun struct_name ctxt = #1 (Names.get ctxt);
+val struct_begin = (Names.map o apfst) (fn _ => "Isabelle" ^ serial_string ());
+
 fun variant a ctxt =
   let
-    val names = Names.get ctxt;
+    val names = #2 (Names.get ctxt);
     val (b, names') = Name.variant (Name.desymbolize (SOME false) a) names;
-    val ctxt' = Names.put names' ctxt;
+    val ctxt' = (Names.map o apsnd) (K names') ctxt;
   in (b, ctxt') end;
 
 
@@ -77,7 +79,7 @@
   let
     val (b, ctxt') = variant a ctxt;
     val env = "val " ^ b ^ " = " ^ s ^ ";\n";
-    val body = "Isabelle." ^ b;
+    val body = struct_name ctxt ^ "." ^ b;
     fun decl (_: Proof.context) = (env, body);
   in (decl, ctxt') end;
 
@@ -118,36 +120,32 @@
   Parse.!!! (Parse.position Parse.xname -- Parse.args --| Scan.ahead Parse.eof)
   >> uncurry Token.src;
 
-val begin_env0 = ML_Lex.tokenize "structure Isabelle =\nstruct\n";
-
-fun begin_env visible =
-  ML_Lex.tokenize
-    ("structure Isabelle =\nstruct\n\
+fun make_env name visible =
+  (ML_Lex.tokenize
+    ("structure " ^ name ^ " =\nstruct\n\
      \val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^
      " (ML_Context.the_local_context ());\n\
      \val ML_print_depth =\n\
      \  let val default = ML_Options.get_print_depth ()\n\
-     \  in fn () => ML_Options.get_print_depth_default default end;\n");
+     \  in fn () => ML_Options.get_print_depth_default default end;\n"),
+   ML_Lex.tokenize "end;");
 
-val end_env = ML_Lex.tokenize "end;";
-val reset_env = ML_Lex.tokenize "structure Isabelle = struct end";
+fun reset_env name = ML_Lex.tokenize ("structure " ^ name ^ " = struct end");
 
 fun expanding (Antiquote.Text tok) = ML_Lex.is_cartouche tok
   | expanding (Antiquote.Antiq _) = true;
 
-in
-
 fun eval_antiquotes (ants, pos) opt_context =
   let
     val visible =
       (case opt_context of
         SOME (Context.Proof ctxt) => Context_Position.is_visible ctxt
       | _ => true);
-    val opt_ctxt = Option.map (Context.Proof o Context.proof_of) opt_context;
+    val opt_ctxt = Option.map Context.proof_of opt_context;
 
     val ((ml_env, ml_body), opt_ctxt') =
       if forall (not o expanding) ants
-      then ((begin_env0, map (fn Antiquote.Text tok => tok) ants), opt_ctxt)
+      then (([], map (fn Antiquote.Text tok => tok) ants), opt_ctxt)
       else
         let
           fun tokenize range = apply2 (ML_Lex.tokenize #> map (ML_Lex.set_range range));
@@ -176,13 +174,16 @@
           val ctxt =
             (case opt_ctxt of
               NONE => error ("No context -- cannot expand ML antiquotations" ^ Position.here pos)
-            | SOME ctxt => Context.proof_of ctxt);
+            | SOME ctxt => struct_begin ctxt);
 
+          val (begin_env, end_env) = make_env (struct_name ctxt) visible;
           val (decls, ctxt') = fold_map expand ants ctxt;
           val (ml_env, ml_body) =
             decls |> map (fn decl => decl ctxt') |> split_list |> apply2 flat;
-        in ((begin_env visible @ ml_env, ml_body), SOME (Context.Proof ctxt')) end;
-  in ((ml_env @ end_env, ml_body), opt_ctxt') end;
+        in ((begin_env @ ml_env @ end_env, ml_body), SOME ctxt') end;
+  in ((ml_env, ml_body), opt_ctxt') end;
+
+in
 
 fun eval flags pos ants =
   let
@@ -191,22 +192,33 @@
     (*prepare source text*)
     val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ());
     val _ =
-      (case Option.map Context.proof_of env_ctxt of
+      (case env_ctxt of
         SOME ctxt =>
           if Config.get ctxt ML_Options.source_trace andalso Context_Position.is_visible ctxt
           then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
           else ()
       | NONE => ());
 
-    (*prepare static ML environment*)
+    (*prepare environment*)
     val _ =
       Context.setmp_thread_data
-        (Option.map (Context.mapping I (Context_Position.set_visible false)) env_ctxt)
+        (Option.map (Context.Proof o Context_Position.set_visible false) env_ctxt)
         (fn () => (ML_Compiler.eval non_verbose Position.none env; Context.thread_data ())) ()
       |> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit context'));
 
+    (*eval body*)
     val _ = ML_Compiler.eval flags pos body;
-    val _ = ML_Compiler.eval non_verbose Position.none reset_env;
+
+    (*clear environment*)
+    val _ =
+      (case (env_ctxt, is_some (Context.thread_data ())) of
+        (SOME ctxt, true) =>
+          let
+            val name = struct_name ctxt;
+            val _ = ML_Compiler.eval non_verbose Position.none (reset_env name);
+            val _ = Context.>> (ML_Env.forget_structure name);
+          in () end
+      | _ => ());
   in () end;
 
 end;
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Pure/ML/ml_env.ML	Wed Dec 10 20:56:33 2014 +0100
@@ -8,6 +8,7 @@
 signature ML_ENV =
 sig
   val inherit: Context.generic -> Context.generic -> Context.generic
+  val forget_structure: string -> Context.generic -> Context.generic
   val name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
   val local_context: use_context
   val local_name_space: ML_Name_Space.T
@@ -63,6 +64,14 @@
 
 val inherit = Env.put o Env.get;
 
+fun forget_structure name =
+  Env.map (fn {bootstrap, tables, sml_tables} =>
+    let
+      val _ = if bootstrap then ML_Name_Space.forget_global_structure name else ();
+      val tables' =
+        (#1 tables, #2 tables, #3 tables, Symtab.delete_safe name (#4 tables), #5 tables, #6 tables);
+    in make_data (bootstrap, tables', sml_tables) end);
+
 
 (* name space *)
 
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML	Wed Dec 10 20:56:33 2014 +0100
@@ -144,20 +144,16 @@
 local
 
 fun token_kind_markup SML =
- fn Keyword => (Markup.empty, "")
-  | Ident => (Markup.empty, "")
-  | Long_Ident => (Markup.empty, "")
-  | Type_Var => (Markup.ML_tvar, "")
+ fn Type_Var => (Markup.ML_tvar, "")
   | Word => (Markup.ML_numeral, "")
   | Int => (Markup.ML_numeral, "")
   | Real => (Markup.ML_numeral, "")
   | Char => (Markup.ML_char, "")
   | String => (if SML then Markup.SML_string else Markup.ML_string, "")
-  | Space => (Markup.empty, "")
   | Cartouche => (Markup.ML_cartouche, "")
   | Comment => (if SML then Markup.SML_comment else Markup.ML_comment, "")
   | Error msg => (Markup.bad, msg)
-  | EOF => (Markup.empty, "");
+  | _ => (Markup.empty, "");
 
 in
 
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Pure/ML/ml_thms.ML	Wed Dec 10 20:56:33 2014 +0100
@@ -58,7 +58,7 @@
     val (name, ctxt') = ML_Context.variant kind ctxt;
     val ctxt'' = cons_thms ((name, is_single), thms) ctxt';
 
-    val ml_body = "Isabelle." ^ name;
+    val ml_body = ML_Context.struct_name ctxt ^ "." ^ name;
     fun decl final_ctxt =
       if initial then
         let
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Pure/PIDE/command.ML	Wed Dec 10 20:56:33 2014 +0100
@@ -162,7 +162,7 @@
         SOME tok => Token.pos_of tok
       | NONE => #1 proper_range);
 
-    val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens span;
+    val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens keywords span;
     val _ = Position.reports_text (token_reports @ maps command_reports span);
   in
     if is_malformed then Toplevel.malformed pos "Malformed command syntax"
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Pure/PIDE/markup.ML	Wed Dec 10 20:56:33 2014 +0100
@@ -202,6 +202,7 @@
   val output: T -> Output.output * Output.output
   val enclose: T -> Output.output -> Output.output
   val markup: T -> string -> string
+  val markups: T list -> string -> string
   val markup_only: T -> string
   val markup_report: string -> string
 end;
@@ -645,6 +646,8 @@
   let val (bg, en) = output m
   in Library.enclose (Output.escape bg) (Output.escape en) end;
 
+val markups = fold_rev markup;
+
 fun markup_only m = markup m "";
 
 fun markup_report "" = ""
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Pure/PIDE/resources.ML	Wed Dec 10 20:56:33 2014 +0100
@@ -158,7 +158,7 @@
     fun init () =
       begin_theory master_dir header parents
       |> Present.begin_theory update_time
-          (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
+          (fn () => HTML.html_mode (implode o map (Thy_Syntax.present_span keywords)) spans);
 
     val (results, thy) =
       cond_timeit true ("theory " ^ quote name)
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Pure/Thy/latex.ML	Wed Dec 10 20:56:33 2014 +0100
@@ -189,8 +189,10 @@
   in (output_symbols syms, Symbol.length syms) end;
 
 fun latex_markup (s, _) =
-  if s = Markup.commandN orelse s = Markup.keyword1N then ("\\isacommand{", "}")
-  else if s = Markup.keyword2N then ("\\isakeyword{", "}")
+  if s = Markup.commandN orelse s = Markup.keyword1N orelse s = Markup.keyword3N
+  then ("\\isacommand{", "}")
+  else if s = Markup.keyword2N
+  then ("\\isakeyword{", "}")
   else Markup.no_output;
 
 fun latex_indent "" _ = ""
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Wed Dec 10 20:56:33 2014 +0100
@@ -6,9 +6,9 @@
 
 signature THY_SYNTAX =
 sig
-  val reports_of_tokens: Token.T list -> bool * Position.report_text list
-  val present_token: Token.T -> Output.output
-  val present_span: Command_Span.span -> Output.output
+  val reports_of_tokens: Keyword.keywords -> Token.T list -> bool * Position.report_text list
+  val present_token: Keyword.keywords -> Token.T -> Output.output
+  val present_span: Keyword.keywords -> Command_Span.span -> Output.output
   datatype 'a element = Element of 'a * ('a element list * 'a) option
   val atom: 'a -> 'a element
   val map_element: ('a -> 'b) -> 'a element -> 'b element
@@ -24,7 +24,7 @@
 
 local
 
-fun reports_of_token tok =
+fun reports_of_token keywords tok =
   let
     val malformed_symbols =
       Input.source_explode (Token.source_position_of tok)
@@ -32,21 +32,21 @@
           if Symbol.is_malformed sym
           then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
     val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
-    val reports = Token.report tok :: Token.completion_report tok @ malformed_symbols;
+    val reports = Token.reports keywords tok @ Token.completion_report tok @ malformed_symbols;
   in (is_malformed, reports) end;
 
 in
 
-fun reports_of_tokens toks =
-  let val results = map reports_of_token toks
+fun reports_of_tokens keywords toks =
+  let val results = map (reports_of_token keywords) toks
   in (exists fst results, maps snd results) end;
 
 end;
 
-fun present_token tok =
-  Markup.enclose (Token.markup tok) (Output.output (Token.unparse tok));
+fun present_token keywords tok =
+  fold_rev Markup.enclose (Token.markups keywords tok) (Output.output (Token.unparse tok));
 
-val present_span = implode o map present_token o Command_Span.content;
+fun present_span keywords = implode o map (present_token keywords) o Command_Span.content;
 
 
 
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Tools/Code/code_runtime.ML	Wed Dec 10 20:56:33 2014 +0100
@@ -359,7 +359,7 @@
     val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt;
     val (ml_code, consts_map) = Lazy.force acc_code;
     val ml_code = if is_first then ml_code else "";
-    val body = "Isabelle." ^ the (AList.lookup (op =) consts_map const);
+    val body = ML_Context.struct_name ctxt ^ "." ^ the (AList.lookup (op =) consts_map const);
   in (ml_code, body) end;
 
 in
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Tools/jEdit/etc/options	Wed Dec 10 20:56:33 2014 +0100
@@ -89,9 +89,8 @@
 option information_color : string = "C1DFEEFF"
 option warning_color : string = "FF8C00FF"
 option error_color : string = "B22222FF"
-option error1_color : string = "B2222232"
 option writeln_message_color : string = "F0F0F0FF"
-option information_message_color : string = "C1DFEE32"
+option information_message_color : string = "DCEAF3FF"
 option tracing_message_color : string = "F0F8FFFF"
 option warning_message_color : string = "EEE8AAFF"
 option error_message_color : string = "FFC1C1FF"
@@ -123,9 +122,9 @@
 option bound_color : string = "008000FF"
 option var_color : string = "00009BFF"
 option inner_numeral_color : string = "FF0000FF"
-option inner_quoted_color : string = "D2691EFF"
+option inner_quoted_color : string = "FF00CCFF"
 option inner_cartouche_color : string = "CC6600FF"
-option inner_comment_color : string = "8B0000FF"
+option inner_comment_color : string = "CC0000FF"
 option dynamic_color : string = "7BA428FF"
 
 
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Wed Dec 10 20:56:33 2014 +0100
@@ -128,27 +128,37 @@
         GUI_Thread.assert {}
 
         val gutter = text_area.getGutter
-        val width = GutterOptionPane.getSelectionAreaWidth
+        val sel_width = GutterOptionPane.getSelectionAreaWidth
         val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
         val FOLD_MARKER_SIZE = 12
 
-        if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
-          val buffer = model.buffer
-          JEdit_Lib.buffer_lock(buffer) {
-            val rendering = get_rendering()
+        val buffer = model.buffer
+        JEdit_Lib.buffer_lock(buffer) {
+          val rendering = get_rendering()
 
-            for (i <- 0 until physical_lines.length) {
-              if (physical_lines(i) != -1) {
-                val line_range = Text.Range(start(i), end(i))
+          for (i <- 0 until physical_lines.length) {
+            if (physical_lines(i) != -1) {
+              val line_range = Text.Range(start(i), end(i))
 
-                // gutter icons
-                rendering.gutter_icon(line_range) match {
-                  case Some(icon) =>
-                    val x0 = (FOLD_MARKER_SIZE + width - border_width - icon.getIconWidth) max 10
-                    val y0 = y + i * line_height + (((line_height - icon.getIconHeight) / 2) max 0)
+              rendering.gutter_content(line_range) match {
+                case Some((icon, color)) =>
+                  // icons within selection area
+                  if (!gutter.isExpanded &&
+                      gutter.isSelectionAreaEnabled && sel_width >= 12 && line_height >= 12)
+                  {
+                    val x0 =
+                      (FOLD_MARKER_SIZE + sel_width - border_width - icon.getIconWidth) max 10
+                    val y0 =
+                      y + i * line_height + (((line_height - icon.getIconHeight) / 2) max 0)
                     icon.paintIcon(gutter, gfx, x0, y0)
-                  case None =>
-                }
+                  }
+                  // background
+                  else {
+                    val y0 = y + i * line_height
+                    gfx.setColor(color)
+                    gfx.fillRect(0, y0, gutter.getWidth, line_height)
+                  }
+                case None =>
               }
             }
           }
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Wed Dec 10 20:56:33 2014 +0100
@@ -53,11 +53,8 @@
     import JEditToken._
     Map[String, Byte](
       Keyword.THY_END -> KEYWORD2,
-      Keyword.QED_SCRIPT -> DIGIT,
-      Keyword.PRF_SCRIPT -> DIGIT,
       Keyword.PRF_ASM -> KEYWORD3,
-      Keyword.PRF_ASM_GOAL -> KEYWORD3,
-      Keyword.PRF_ASM_GOAL_SCRIPT -> DIGIT
+      Keyword.PRF_ASM_GOAL -> KEYWORD3
     ).withDefaultValue(KEYWORD1)
   }
 
@@ -135,7 +132,7 @@
   private val language_context_elements =
     Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
       Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
-      Markup.ML_STRING, Markup.ML_COMMENT)
+      Markup.ML_STRING, Markup.ML_CARTOUCHE, Markup.ML_COMMENT)
 
   private val language_elements = Markup.Elements(Markup.LANGUAGE)
 
@@ -226,7 +223,6 @@
   val information_color = color_value("information_color")
   val warning_color = color_value("warning_color")
   val error_color = color_value("error_color")
-  val error1_color = color_value("error1_color")
   val writeln_message_color = color_value("writeln_message_color")
   val information_message_color = color_value("information_message_color")
   val tracing_message_color = color_value("tracing_message_color")
@@ -285,7 +281,9 @@
           if (delimited) Some(Completion.Language_Context(language, symbols, antiquotes))
           else None
         case Text.Info(_, elem)
-        if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
+        if elem.name == Markup.ML_STRING ||
+          elem.name == Markup.ML_CARTOUCHE ||
+          elem.name == Markup.ML_COMMENT =>
           Some(Completion.Language_Context.ML_inner)
         case Text.Info(_, _) =>
           Some(Completion.Language_Context.inner)
@@ -553,13 +551,17 @@
     else if (Protocol.is_information(msg)) Rendering.information_pri
     else 0
 
-  private lazy val gutter_icons = Map(
-    Rendering.information_pri -> JEdit_Lib.load_icon(options.string("gutter_information_icon")),
-    Rendering.warning_pri -> JEdit_Lib.load_icon(options.string("gutter_warning_icon")),
-    Rendering.legacy_pri -> JEdit_Lib.load_icon(options.string("gutter_legacy_icon")),
-    Rendering.error_pri -> JEdit_Lib.load_icon(options.string("gutter_error_icon")))
+  private lazy val gutter_message_content = Map(
+    Rendering.information_pri ->
+      (JEdit_Lib.load_icon(options.string("gutter_information_icon")), information_message_color),
+    Rendering.warning_pri ->
+      (JEdit_Lib.load_icon(options.string("gutter_warning_icon")), warning_message_color),
+    Rendering.legacy_pri ->
+      (JEdit_Lib.load_icon(options.string("gutter_legacy_icon")), warning_message_color),
+    Rendering.error_pri ->
+      (JEdit_Lib.load_icon(options.string("gutter_error_icon")), error_message_color))
 
-  def gutter_icon(range: Text.Range): Option[Icon] =
+  def gutter_content(range: Text.Range): Option[(Icon, Color)] =
   {
     val pris =
       snapshot.cumulate[Int](range, 0, Rendering.gutter_elements, _ =>
@@ -569,7 +571,7 @@
           case _ => None
         }).map(_.info)
 
-    gutter_icons.get((0 /: pris)(_ max _))
+    gutter_message_content.get((0 /: pris)(_ max _))
   }
 
 
diff -r f65ac77f7e07 -r f4b6e2626cf8 src/Tools/jEdit/src/structure_matching.scala
--- a/src/Tools/jEdit/src/structure_matching.scala	Tue Dec 09 16:22:40 2014 +0100
+++ b/src/Tools/jEdit/src/structure_matching.scala	Wed Dec 10 20:56:33 2014 +0100
@@ -45,7 +45,7 @@
           val limit = PIDE.options.value.int("jedit_structure_limit") max 0
 
           def is_command_kind(token: Token, pred: String => Boolean): Boolean =
-            syntax.keywords.is_command_kind(token, pred)
+            token.is_command_kind(syntax.keywords, pred)
 
           def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
             Token_Markup.line_token_iterator(syntax, buffer, line, line + lim).