# HG changeset patch # User wenzelm # Date 1426194446 -3600 # Node ID 68996aa778299ac48c1ebbdc5204e4356d013126 # Parent f24ab09e4c37414f6384693e5901c218d8bf2553# Parent c043306d2598710f43984dcb4e84a9f4ddfc4e30 merged diff -r f24ab09e4c37 -r 68996aa77829 src/HOL/Bali/DeclConcepts.thy --- 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 \ (qtname \ methd) \ (qtname \ memberdecl)" + "method" :: "sig \ (qtname \ methd) \ (qtname \ memberdecl)" where "method sig m = (declclass m, mdecl (sig, mthd m))" lemma method_simp[simp]: "method sig (C,m) = (C,mdecl (sig,m))" diff -r f24ab09e4c37 -r 68996aa77829 src/HOL/MicroJava/BV/BVNoTypeError.thy --- 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 ("\") and Phi ("\") assumes wt: "wt_jvm_prog \ \" assumes is_class: "is_class \ C" - and method: "method (\,C) (m,[]) = Some (C, b)" + and "method": "method (\,C) (m,[]) = Some (C, b)" and m: "m \ init" defines start: "s \ start_state \ C m" assumes s: "\ \ (Normal s) \jvmd\ t" shows "t \ TypeError" proof - - from wt is_class method have "\,\ \JVM s \" + from wt is_class "method" have "\,\ \JVM s \" 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 ("\") and Phi ("\") assumes wt: "wt_jvm_prog \ \" assumes is_class: "is_class \ C" - and method: "method (\,C) (m,[]) = Some (C, b)" + and "method": "method (\,C) (m,[]) = Some (C, b)" and m: "m \ init" defines start: "s \ start_state \ C m" shows "\ \ (Normal s) \jvmd\ (Normal t) = \ \ s \jvm\ t" proof - - from wt is_class method have "\,\ \JVM s \" + from wt is_class "method" have "\,\ \JVM s \" unfolding start by (rule BV_correct_initial) with wt show ?thesis by (rule welltyped_commutes) qed diff -r f24ab09e4c37 -r 68996aa77829 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy --- 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 @@ \ G,phi \JVM state'\" 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\h hp\" 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) diff -r f24ab09e4c37 -r 68996aa77829 src/HOL/MicroJava/J/TypeRel.thy --- 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 \ cname => ( sig \ cname \ ty \ 'c)" (* ###curry *) + "method" :: "'c prog \ cname => ( sig \ cname \ ty \ 'c)" (* ###curry *) field :: "'c prog \ cname => ( vname \ cname \ ty )" (* ###curry *) fields :: "'c prog \ cname => ((vname \ cname) \ ty) list" (* ###curry *) diff -r f24ab09e4c37 -r 68996aa77829 src/HOL/NanoJava/TypeRel.thy --- 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 \ methd)" where +definition "method" :: "cname => (mname \ methd)" where "method C \ class_rec C methods" lemma method_rec: "\class C = Some m; ws_prog\ \ diff -r f24ab09e4c37 -r 68996aa77829 src/Pure/Isar/outer_syntax.scala --- 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() } } diff -r f24ab09e4c37 -r 68996aa77829 src/Pure/PIDE/command.ML --- 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 diff -r f24ab09e4c37 -r 68996aa77829 src/Pure/PIDE/command.scala --- 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, diff -r f24ab09e4c37 -r 68996aa77829 src/Pure/PIDE/command_span.ML --- 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 diff -r f24ab09e4c37 -r 68996aa77829 src/Pure/PIDE/command_span.scala --- 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) } } - diff -r f24ab09e4c37 -r 68996aa77829 src/Pure/PIDE/document.ML --- 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 = diff -r f24ab09e4c37 -r 68996aa77829 src/Pure/PIDE/protocol.ML --- 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 _ = diff -r f24ab09e4c37 -r 68996aa77829 src/Pure/PIDE/protocol.scala --- 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 diff -r f24ab09e4c37 -r 68996aa77829 src/Pure/PIDE/resources.scala --- 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 diff -r f24ab09e4c37 -r 68996aa77829 src/Pure/Thy/thy_syntax.scala --- 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) } }