--- a/src/HOL/Bali/DeclConcepts.thy Thu Mar 12 19:09:18 2015 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy Thu Mar 12 22:07:26 2015 +0100
@@ -368,7 +368,7 @@
class) to a qualified member declaration: @{text method} *}
definition
- method :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)"
+ "method" :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)"
where "method sig m = (declclass m, mdecl (sig, mthd m))"
lemma method_simp[simp]: "method sig (C,m) = (C,mdecl (sig,m))"
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy Thu Mar 12 19:09:18 2015 +0100
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy Thu Mar 12 22:07:26 2015 +0100
@@ -429,14 +429,14 @@
fixes G ("\<Gamma>") and Phi ("\<Phi>")
assumes wt: "wt_jvm_prog \<Gamma> \<Phi>"
assumes is_class: "is_class \<Gamma> C"
- and method: "method (\<Gamma>,C) (m,[]) = Some (C, b)"
+ and "method": "method (\<Gamma>,C) (m,[]) = Some (C, b)"
and m: "m \<noteq> init"
defines start: "s \<equiv> start_state \<Gamma> C m"
assumes s: "\<Gamma> \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> t"
shows "t \<noteq> TypeError"
proof -
- from wt is_class method have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
+ from wt is_class "method" have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
unfolding start by (rule BV_correct_initial)
from wt this s show ?thesis by (rule no_type_errors)
qed
@@ -461,12 +461,12 @@
fixes G ("\<Gamma>") and Phi ("\<Phi>")
assumes wt: "wt_jvm_prog \<Gamma> \<Phi>"
assumes is_class: "is_class \<Gamma> C"
- and method: "method (\<Gamma>,C) (m,[]) = Some (C, b)"
+ and "method": "method (\<Gamma>,C) (m,[]) = Some (C, b)"
and m: "m \<noteq> init"
defines start: "s \<equiv> start_state \<Gamma> C m"
shows "\<Gamma> \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> (Normal t) = \<Gamma> \<turnstile> s \<midarrow>jvm\<rightarrow> t"
proof -
- from wt is_class method have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
+ from wt is_class "method" have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
unfolding start by (rule BV_correct_initial)
with wt show ?thesis by (rule welltyped_commutes)
qed
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Thu Mar 12 19:09:18 2015 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Thu Mar 12 22:07:26 2015 +0100
@@ -811,7 +811,7 @@
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
proof -
assume wtprog: "wt_jvm_prog G phi"
- assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
+ assume "method": "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
assume ins: "ins ! pc = Invoke C' mn pTs"
assume wti: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
assume state': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)"
@@ -823,7 +823,7 @@
wfprog: "wf_prog wfmb G"
by (simp add: wt_jvm_prog_def)
- from ins method approx
+ from ins "method" approx
obtain s where
heap_ok: "G\<turnstile>h hp\<surd>" and
prealloc:"preallocated hp" and
@@ -880,7 +880,7 @@
from stk' l_o l
have oX_pos: "last (take (Suc (length pTs)) stk) = oX" by simp
- with state' method ins no_xcp oX_conf
+ with state' "method" ins no_xcp oX_conf
obtain ref where oX_Addr: "oX = Addr ref"
by (auto simp add: raise_system_xcpt_def dest: conf_RefTD)
@@ -922,7 +922,7 @@
from loc obj_ty have "fst (the (hp ref)) = D" by (simp add: obj_ty_def)
- with oX_Addr oX_pos state' method ins stk' l_o l loc obj_ty mD no_xcp
+ with oX_Addr oX_pos state' "method" ins stk' l_o l loc obj_ty mD no_xcp
have state'_val:
"state' =
Norm (hp, ([], Addr ref # rev opTs @ replicate mxl' undefined,
@@ -972,7 +972,7 @@
show ?thesis by (simp add: correct_frame_def)
qed
- from state'_val heap_ok mD'' ins method phi_pc s X' l mX
+ from state'_val heap_ok mD'' ins "method" phi_pc s X' l mX
frames s' LT0 c_f is_class_C stk' oX_Addr frame prealloc and l
show ?thesis
apply (simp add: correct_state_def)
--- a/src/HOL/MicroJava/J/TypeRel.thy Thu Mar 12 19:09:18 2015 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy Thu Mar 12 22:07:26 2015 +0100
@@ -177,7 +177,7 @@
qed
consts
- method :: "'c prog \<times> cname => ( sig \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
+ "method" :: "'c prog \<times> cname => ( sig \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
field :: "'c prog \<times> cname => ( vname \<rightharpoonup> cname \<times> ty )" (* ###curry *)
fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
--- a/src/HOL/NanoJava/TypeRel.thy Thu Mar 12 19:09:18 2015 +0100
+++ b/src/HOL/NanoJava/TypeRel.thy Thu Mar 12 22:07:26 2015 +0100
@@ -108,7 +108,7 @@
done
--{* Methods of a class, with inheritance and hiding *}
-definition method :: "cname => (mname \<rightharpoonup> methd)" where
+definition "method" :: "cname => (mname \<rightharpoonup> methd)" where
"method C \<equiv> class_rec C methods"
lemma method_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
--- a/src/Pure/Isar/outer_syntax.scala Thu Mar 12 19:09:18 2015 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Thu Mar 12 22:07:26 2015 +0100
@@ -284,7 +284,7 @@
/* result structure */
val spans = parse_spans(text)
- spans.foreach(span => add(Command(Document_ID.none, node_name, Nil, span)))
+ spans.foreach(span => add(Command(Document_ID.none, node_name, None, span)))
result()
}
}
--- a/src/Pure/PIDE/command.ML Thu Mar 12 19:09:18 2015 +0100
+++ b/src/Pure/PIDE/command.ML Thu Mar 12 22:07:26 2015 +0100
@@ -51,21 +51,19 @@
fun read_file_node file_node master_dir pos src_path =
let
- val _ = Position.report pos Markup.language_path;
val _ =
(case try Url.explode file_node of
NONE => ()
| SOME (Url.File _) => ()
| _ =>
- (Position.report pos (Markup.path file_node);
error ("Prover cannot load remote file " ^
- Markup.markup (Markup.path file_node) (quote file_node) ^ Position.here pos)));
+ Markup.markup (Markup.path file_node) (quote file_node)));
val full_path = File.check_file (File.full_path master_dir src_path);
- val _ = Position.report pos (Markup.path (Path.implode full_path));
val text = File.read full_path;
val lines = split_lines text;
val digest = SHA1.digest text;
- in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end;
+ in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end
+ handle ERROR msg => error (msg ^ Position.here pos);
val read_file = read_file_node "";
@@ -89,8 +87,7 @@
Exn.interruptible_capture (fn () =>
read_file_node file_node master_dir pos src_path) ()
| make_file src_path (Exn.Res (file_node, SOME (digest, lines))) =
- (Position.reports [(pos, Markup.language_path), (pos, Markup.path file_node)];
- Exn.Res (blob_file src_path lines digest file_node))
+ Exn.Res (blob_file src_path lines digest file_node)
| make_file _ (Exn.Exn e) = Exn.Exn e;
val src_paths = Keyword.command_files keywords cmd path;
in
--- a/src/Pure/PIDE/command.scala Thu Mar 12 19:09:18 2015 +0100
+++ b/src/Pure/PIDE/command.scala Thu Mar 12 22:07:26 2015 +0100
@@ -253,15 +253,17 @@
def apply(
id: Document_ID.Command,
node_name: Document.Node.Name,
- blobs: List[Blob],
+ blobs: Option[(List[Blob], Int)],
span: Command_Span.Span): Command =
{
val (source, span1) = span.compact_source
- new Command(id, node_name, blobs, span1, source, Results.empty, Markup_Tree.empty)
+ val (blobs_list, blobs_index) = blobs.getOrElse((Nil, -1))
+ new Command(
+ id, node_name, blobs_list, blobs_index, span1, source, Results.empty, Markup_Tree.empty)
}
val empty: Command =
- Command(Document_ID.none, Document.Node.Name.empty, Nil, Command_Span.empty)
+ Command(Document_ID.none, Document.Node.Name.empty, None, Command_Span.empty)
def unparsed(
id: Document_ID.Command,
@@ -270,7 +272,7 @@
markup: Markup_Tree): Command =
{
val (source1, span1) = Command_Span.unparsed(source).compact_source
- new Command(id, Document.Node.Name.empty, Nil, span1, source1, results, markup)
+ new Command(id, Document.Node.Name.empty, Nil, -1, span1, source1, results, markup)
}
def unparsed(source: String): Command =
@@ -312,6 +314,7 @@
val id: Document_ID.Command,
val node_name: Document.Node.Name,
val blobs: List[Command.Blob],
+ val blobs_index: Int,
val span: Command_Span.Span,
val source: String,
val init_results: Command.Results,
--- a/src/Pure/PIDE/command_span.ML Thu Mar 12 19:09:18 2015 +0100
+++ b/src/Pure/PIDE/command_span.ML Thu Mar 12 22:07:26 2015 +0100
@@ -28,22 +28,20 @@
local
-fun clean ((i1, t1) :: (i2, t2) :: toks) =
- if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean toks
- else (i1, t1) :: clean ((i2, t2) :: toks)
+fun clean ((t1, i1) :: (t2, i2) :: rest) =
+ if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean rest
+ else (t1, i1) :: clean ((t2, i2) :: rest)
| clean toks = toks;
-fun clean_tokens toks =
- ((0 upto length toks - 1) ~~ toks)
- |> filter (fn (_, tok) => Token.is_proper tok)
- |> clean;
+fun clean_tokens tokens =
+ clean (filter (fn (t, _) => Token.is_proper t) (tokens ~~ (0 upto length tokens - 1)));
-fun find_file ((_, tok) :: toks) =
+fun find_file ((tok, _) :: toks) =
if Token.is_command tok then
- toks |> get_first (fn (i, tok) =>
- if Token.is_name tok then
- SOME (i, (Path.explode (Token.content_of tok), Token.pos_of tok))
- handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok))
+ toks |> get_first (fn (t, i) =>
+ if Token.is_name t then
+ SOME ((Path.explode (Token.content_of t), Token.pos_of t), i)
+ handle ERROR msg => error (msg ^ Position.here (Token.pos_of t))
else NONE)
else NONE
| find_file [] = NONE;
@@ -56,7 +54,7 @@
if Keyword.is_theory_load keywords cmd then
(case find_file (clean_tokens toks) of
NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
- | SOME (i, path) =>
+ | SOME (path, i) =>
let
val toks' = toks |> map_index (fn (j, tok) =>
if i = j then Token.put_files (read_files cmd path) tok
--- a/src/Pure/PIDE/command_span.scala Thu Mar 12 19:09:18 2015 +0100
+++ b/src/Pure/PIDE/command_span.scala Thu Mar 12 22:07:26 2015 +0100
@@ -56,34 +56,41 @@
/* resolve inlined files */
- private def find_file(tokens: List[Token]): Option[String] =
+ private def clean_tokens(tokens: List[Token]): List[(Token, Int)] =
{
- def clean(toks: List[Token]): List[Token] =
+ def clean(toks: List[(Token, Int)]): List[(Token, Int)] =
toks match {
- case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
- case t :: ts => t :: clean(ts)
- case Nil => Nil
+ case (t1, i1) :: (t2, i2) :: rest =>
+ if (t1.is_keyword && (t1.source == "%" || t1.source == "--")) clean(rest)
+ else (t1, i1) :: clean((t2, i2) :: rest)
+ case _ => toks
}
- clean(tokens.filter(_.is_proper)) match {
- case tok :: toks if tok.is_command => toks.find(_.is_name).map(_.content)
- case _ => None
- }
+ clean(tokens.zipWithIndex.filter({ case (t, _) => t.is_proper }))
}
- def span_files(syntax: Prover.Syntax, span: Span): List[String] =
+ private def find_file(tokens: List[(Token, Int)]): Option[(String, Int)] =
+ tokens match {
+ case (tok, _) :: toks =>
+ if (tok.is_command)
+ toks.collectFirst({ case (t, i) if t.is_name => (t.content, i) })
+ else None
+ case Nil => None
+ }
+
+ def span_files(syntax: Prover.Syntax, span: Span): (List[String], Int) =
span.kind match {
case Command_Span(name, _) =>
syntax.load_command(name) match {
case Some(exts) =>
- find_file(span.content) match {
- case Some(file) =>
- if (exts.isEmpty) List(file)
- else exts.map(ext => file + "." + ext)
- case None => Nil
+ find_file(clean_tokens(span.content)) match {
+ case Some((file, i)) =>
+ if (exts.isEmpty) (List(file), i)
+ else (exts.map(ext => file + "." + ext), i)
+ case None => (Nil, -1)
}
- case None => Nil
+ case None => (Nil, -1)
}
- case _ => Nil
+ case _ => (Nil, -1)
}
def resolve_files(
@@ -92,15 +99,17 @@
node_name: Document.Node.Name,
span: Span,
get_blob: Document.Node.Name => Option[Document.Blob])
- : List[Command.Blob] =
+ : (List[Command.Blob], Int) =
{
- span_files(syntax, span).map(file_name =>
- Exn.capture {
- val name =
- Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
- val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
- (name, blob)
- })
+ val (files, index) = span_files(syntax, span)
+ val blobs =
+ files.map(file =>
+ Exn.capture {
+ val name =
+ Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file)))
+ val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
+ (name, blob)
+ })
+ (blobs, index)
}
}
-
--- a/src/Pure/PIDE/document.ML Thu Mar 12 19:09:18 2015 +0100
+++ b/src/Pure/PIDE/document.ML Thu Mar 12 22:07:26 2015 +0100
@@ -19,7 +19,7 @@
val init_state: state
val define_blob: string -> string -> state -> state
type blob_digest = (string * string option) Exn.result
- val define_command: Document_ID.command -> string -> blob_digest list ->
+ val define_command: Document_ID.command -> string -> blob_digest list -> int ->
((int * int) * string) list -> state -> state
val remove_versions: Document_ID.version list -> state -> state
val start_execution: state -> state
@@ -359,23 +359,37 @@
blob_digest |> Exn.map_result (fn (file_node, raw_digest) =>
(file_node, Option.map (the_blob state) raw_digest));
+fun blob_reports pos (blob_digest: blob_digest) =
+ (case blob_digest of Exn.Res (file_node, _) => [(pos, Markup.path file_node)] | _ => []);
+
(* commands *)
-fun define_command command_id name command_blobs toks =
+fun define_command command_id name command_blobs blobs_index toks =
map_state (fn (versions, blobs, commands, execution) =>
let
val id = Document_ID.print command_id;
val span =
Lazy.lazy (fn () =>
Position.setmp_thread_data (Position.id_only id)
- (fn () => #1 (fold_map Token.make toks (Position.id id))) ());
+ (fn () =>
+ let
+ val (tokens, _) = fold_map Token.make toks (Position.id id);
+ val _ =
+ (case try (Token.pos_of o nth tokens) blobs_index of
+ SOME pos =>
+ if Position.is_reported pos then
+ Position.reports
+ ((pos, Markup.language_path) :: maps (blob_reports pos) command_blobs)
+ else ()
+ | NONE => ());
+ in tokens end) ());
+ val commands' =
+ Inttab.update_new (command_id, (name, command_blobs, span)) commands
+ handle Inttab.DUP dup => err_dup "command" dup;
val _ =
Position.setmp_thread_data (Position.id_only id)
(fn () => Output.status (Markup.markup_only Markup.accepted)) ();
- val commands' =
- Inttab.update_new (command_id, (name, command_blobs, span)) commands
- handle Inttab.DUP dup => err_dup "command" dup;
in (versions, blobs, commands', execution) end);
fun the_command (State {commands, ...}) command_id =
--- a/src/Pure/PIDE/protocol.ML Thu Mar 12 19:09:18 2015 +0100
+++ b/src/Pure/PIDE/protocol.ML Thu Mar 12 22:07:26 2015 +0100
@@ -30,17 +30,20 @@
Isabelle_Process.protocol_command "Document.define_command"
(fn id :: name :: blobs_yxml :: toks_yxml :: sources =>
let
- val blobs =
+ val (blobs, blobs_index) =
YXML.parse_body blobs_yxml |>
let open XML.Decode in
- list (variant
- [fn ([], a) => Exn.Res (pair string (option string) a),
- fn ([], a) => Exn.Exn (ERROR (YXML.string_of_body a))])
+ pair
+ (list (variant
+ [fn ([], a) => Exn.Res (pair string (option string) a),
+ fn ([], a) => Exn.Exn (ERROR (YXML.string_of_body a))]))
+ int
end;
val toks =
(YXML.parse_body toks_yxml |> let open XML.Decode in list (pair int int) end) ~~ sources;
in
- Document.change_state (Document.define_command (Document_ID.parse id) name blobs toks)
+ Document.change_state
+ (Document.define_command (Document_ID.parse id) name blobs blobs_index toks)
end);
val _ =
--- a/src/Pure/PIDE/protocol.scala Thu Mar 12 19:09:18 2015 +0100
+++ b/src/Pure/PIDE/protocol.scala Thu Mar 12 22:07:26 2015 +0100
@@ -392,7 +392,7 @@
(Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
{ case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
- YXML.string_of_body(list(encode_blob)(command.blobs))
+ YXML.string_of_body(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
}
val toks = command.span.content
--- a/src/Pure/PIDE/resources.scala Thu Mar 12 19:09:18 2015 +0100
+++ b/src/Pure/PIDE/resources.scala Thu Mar 12 22:07:26 2015 +0100
@@ -57,7 +57,7 @@
def loaded_files(syntax: Prover.Syntax, text: String): List[String] =
if (syntax.load_commands_in(text)) {
val spans = syntax.parse_spans(text)
- spans.iterator.map(Command_Span.span_files(syntax, _)).flatten.toList
+ spans.iterator.map(Command_Span.span_files(syntax, _)._1).flatten.toList
}
else Nil
--- a/src/Pure/Thy/thy_syntax.scala Thu Mar 12 19:09:18 2015 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Thu Mar 12 22:07:26 2015 +0100
@@ -143,8 +143,8 @@
@tailrec private def chop_common(
cmds: List[Command],
- blobs_spans: List[(List[Command.Blob], Command_Span.Span)])
- : (List[Command], List[(List[Command.Blob], Command_Span.Span)]) =
+ blobs_spans: List[((List[Command.Blob], Int), Command_Span.Span)])
+ : (List[Command], List[((List[Command.Blob], Int), Command_Span.Span)]) =
{
(cmds, blobs_spans) match {
case (cmd :: cmds, (blobs, span) :: rest) if cmd.blobs == blobs && cmd.span == span =>
@@ -179,7 +179,8 @@
case cmd :: _ =>
val hook = commands.prev(cmd)
val inserted =
- blobs_spans2.map({ case (blobs, span) => Command(Document_ID.make(), name, blobs, span) })
+ blobs_spans2.map({ case (blobs, span) =>
+ Command(Document_ID.make(), name, Some(blobs), span) })
(commands /: cmds2)(_ - _).append_after(hook, inserted)
}
}