--- 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; }
-
--- 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
--- 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
--- 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
*)
--- 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);
--- 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
--- 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;
--- 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 */
--- 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)
}
--- 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;
--- 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
--- 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;
--- 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 ())))))";
--- 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*)
--- 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)) #>
--- 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;
--- 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 *)
--- 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
--- 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
--- 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"
--- 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 "" = ""
--- 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)
--- 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 "" _ = ""
--- 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;
--- 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
--- 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"
--- 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 =>
}
}
}
--- 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 _))
}
--- 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).