simplified Command.resolve_files in ML, using blobs_index from Scala;
authorwenzelm
Fri Mar 13 12:58:49 2015 +0100 (2015-03-13 ago)
changeset 596897968c57ea240
parent 59688 6c896dfef33b
child 59690 46b635624feb
simplified Command.resolve_files in ML, using blobs_index from Scala;
clarified modules;
src/Pure/PIDE/command.ML
src/Pure/PIDE/command.scala
src/Pure/PIDE/command_span.ML
src/Pure/PIDE/command_span.scala
src/Pure/PIDE/document.ML
src/Pure/PIDE/resources.ML
src/Pure/PIDE/resources.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/PIDE/command.ML	Fri Mar 13 12:44:16 2015 +0100
     1.2 +++ b/src/Pure/PIDE/command.ML	Fri Mar 13 12:58:49 2015 +0100
     1.3 @@ -10,14 +10,14 @@
     1.4    val read_file: Path.T -> Position.T -> Path.T -> Token.file
     1.5    val read_thy: Toplevel.state -> theory
     1.6    val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) ->
     1.7 -    blob list -> Token.T list -> Toplevel.transition
     1.8 +    blob list * int -> Token.T list -> Toplevel.transition
     1.9    type eval
    1.10    val eval_eq: eval * eval -> bool
    1.11    val eval_running: eval -> bool
    1.12    val eval_finished: eval -> bool
    1.13    val eval_result_state: eval -> Toplevel.state
    1.14    val eval: Keyword.keywords -> Path.T -> (unit -> theory) ->
    1.15 -    blob list -> Token.T list -> eval -> eval
    1.16 +    blob list * int -> Token.T list -> eval -> eval
    1.17    type print
    1.18    val print: bool -> (string * string list) list -> Keyword.keywords -> string ->
    1.19      eval -> print list -> print list option
    1.20 @@ -78,26 +78,33 @@
    1.21        | SOME exec_id => Position.put_id exec_id);
    1.22    in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end
    1.23  
    1.24 -fun resolve_files keywords master_dir blobs toks =
    1.25 +fun resolve_files keywords master_dir (blobs, blobs_index) toks =
    1.26    (case Outer_Syntax.parse_spans toks of
    1.27 -    [span] => span
    1.28 -      |> Command_Span.resolve_files keywords (fn cmd => fn (path, pos) =>
    1.29 -        let
    1.30 -          fun make_file src_path (Exn.Res (file_node, NONE)) =
    1.31 -                Exn.interruptible_capture (fn () =>
    1.32 -                  read_file_node file_node master_dir pos src_path) ()
    1.33 -            | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) =
    1.34 -                Exn.Res (blob_file src_path lines digest file_node)
    1.35 -            | make_file _ (Exn.Exn e) = Exn.Exn e;
    1.36 -          val src_paths = Keyword.command_files keywords cmd path;
    1.37 -        in
    1.38 -          if null blobs then
    1.39 -            map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths)
    1.40 -          else if length src_paths = length blobs then
    1.41 -            map2 make_file src_paths blobs
    1.42 -          else error ("Misalignment of inlined files" ^ Position.here pos)
    1.43 -        end)
    1.44 -      |> Command_Span.content
    1.45 +    [Command_Span.Span (Command_Span.Command_Span (cmd, _), _)] =>
    1.46 +      (case try (nth toks) blobs_index of
    1.47 +        SOME tok =>
    1.48 +          let
    1.49 +            val pos = Token.pos_of tok;
    1.50 +            val path = Path.explode (Token.content_of tok)
    1.51 +              handle ERROR msg => error (msg ^ Position.here pos);
    1.52 +            fun make_file src_path (Exn.Res (file_node, NONE)) =
    1.53 +                  Exn.interruptible_capture (fn () =>
    1.54 +                    read_file_node file_node master_dir pos src_path) ()
    1.55 +              | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) =
    1.56 +                  Exn.Res (blob_file src_path lines digest file_node)
    1.57 +              | make_file _ (Exn.Exn e) = Exn.Exn e;
    1.58 +            val src_paths = Keyword.command_files keywords cmd path;
    1.59 +            val files =
    1.60 +              if null blobs then
    1.61 +                map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths)
    1.62 +              else if length src_paths = length blobs then
    1.63 +                map2 make_file src_paths blobs
    1.64 +              else error ("Misalignment of inlined files" ^ Position.here pos);
    1.65 +          in
    1.66 +            toks |> map_index (fn (i, tok) =>
    1.67 +              if i = blobs_index then Token.put_files files tok else tok)
    1.68 +          end
    1.69 +      | NONE => toks)
    1.70    | _ => toks);
    1.71  
    1.72  val bootstrap_thy = ML_Context.the_global_context ();
    1.73 @@ -106,7 +113,7 @@
    1.74  
    1.75  fun read_thy st = Toplevel.theory_of st handle Toplevel.UNDEF => bootstrap_thy;
    1.76  
    1.77 -fun read keywords thy master_dir init blobs span =
    1.78 +fun read keywords thy master_dir init blobs_info span =
    1.79    let
    1.80      val command_reports = Outer_Syntax.command_reports thy;
    1.81  
    1.82 @@ -121,7 +128,7 @@
    1.83    in
    1.84      if is_malformed then Toplevel.malformed pos "Malformed command syntax"
    1.85      else
    1.86 -      (case Outer_Syntax.parse_tokens thy (resolve_files keywords master_dir blobs span) of
    1.87 +      (case Outer_Syntax.parse_tokens thy (resolve_files keywords master_dir blobs_info span) of
    1.88          [tr] => Toplevel.modify_init init tr
    1.89        | [] => Toplevel.ignored (#1 (Token.range_of span))
    1.90        | _ => Toplevel.malformed (#1 proper_range) "Exactly one command expected")
    1.91 @@ -218,7 +225,7 @@
    1.92  
    1.93  in
    1.94  
    1.95 -fun eval keywords master_dir init blobs span eval0 =
    1.96 +fun eval keywords master_dir init blobs_info span eval0 =
    1.97    let
    1.98      val exec_id = Document_ID.make ();
    1.99      fun process () =
   1.100 @@ -227,7 +234,8 @@
   1.101          val thy = read_thy (#state eval_state0);
   1.102          val tr =
   1.103            Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
   1.104 -            (fn () => read keywords thy master_dir init blobs span |> Toplevel.exec_id exec_id) ();
   1.105 +            (fn () =>
   1.106 +              read keywords thy master_dir init blobs_info span |> Toplevel.exec_id exec_id) ();
   1.107        in eval_state keywords span tr eval_state0 end;
   1.108    in Eval {exec_id = exec_id, eval_process = Lazy.lazy process} end;
   1.109  
     2.1 --- a/src/Pure/PIDE/command.scala	Fri Mar 13 12:44:16 2015 +0100
     2.2 +++ b/src/Pure/PIDE/command.scala	Fri Mar 13 12:58:49 2015 +0100
     2.3 @@ -307,6 +307,66 @@
     2.4          (cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
     2.5      }
     2.6    }
     2.7 +
     2.8 +
     2.9 +  /* resolve inlined files */
    2.10 +
    2.11 +  private def clean_tokens(tokens: List[Token]): List[(Token, Int)] =
    2.12 +  {
    2.13 +    def clean(toks: List[(Token, Int)]): List[(Token, Int)] =
    2.14 +      toks match {
    2.15 +        case (t1, i1) :: (t2, i2) :: rest =>
    2.16 +          if (t1.is_keyword && (t1.source == "%" || t1.source == "--")) clean(rest)
    2.17 +          else (t1, i1) :: clean((t2, i2) :: rest)
    2.18 +        case _ => toks
    2.19 +      }
    2.20 +    clean(tokens.zipWithIndex.filter({ case (t, _) => t.is_proper }))
    2.21 +  }
    2.22 +
    2.23 +  private def find_file(tokens: List[(Token, Int)]): Option[(String, Int)] =
    2.24 +    tokens match {
    2.25 +      case (tok, _) :: toks =>
    2.26 +        if (tok.is_command)
    2.27 +          toks.collectFirst({ case (t, i) if t.is_name => (t.content, i) })
    2.28 +        else None
    2.29 +      case Nil => None
    2.30 +    }
    2.31 +
    2.32 +  def span_files(syntax: Prover.Syntax, span: Command_Span.Span): (List[String], Int) =
    2.33 +    span.kind match {
    2.34 +      case Command_Span.Command_Span(name, _) =>
    2.35 +        syntax.load_command(name) match {
    2.36 +          case Some(exts) =>
    2.37 +            find_file(clean_tokens(span.content)) match {
    2.38 +              case Some((file, i)) =>
    2.39 +                if (exts.isEmpty) (List(file), i)
    2.40 +                else (exts.map(ext => file + "." + ext), i)
    2.41 +              case None => (Nil, -1)
    2.42 +            }
    2.43 +          case None => (Nil, -1)
    2.44 +        }
    2.45 +      case _ => (Nil, -1)
    2.46 +    }
    2.47 +
    2.48 +  def resolve_files(
    2.49 +      resources: Resources,
    2.50 +      syntax: Prover.Syntax,
    2.51 +      node_name: Document.Node.Name,
    2.52 +      span: Command_Span.Span,
    2.53 +      get_blob: Document.Node.Name => Option[Document.Blob])
    2.54 +    : (List[Command.Blob], Int) =
    2.55 +  {
    2.56 +    val (files, index) = span_files(syntax, span)
    2.57 +    val blobs =
    2.58 +      files.map(file =>
    2.59 +        Exn.capture {
    2.60 +          val name =
    2.61 +            Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file)))
    2.62 +          val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
    2.63 +          (name, blob)
    2.64 +        })
    2.65 +    (blobs, index)
    2.66 +  }
    2.67  }
    2.68  
    2.69  
     3.1 --- a/src/Pure/PIDE/command_span.ML	Fri Mar 13 12:44:16 2015 +0100
     3.2 +++ b/src/Pure/PIDE/command_span.ML	Fri Mar 13 12:58:49 2015 +0100
     3.3 @@ -10,8 +10,6 @@
     3.4    datatype span = Span of kind * Token.T list
     3.5    val kind: span -> kind
     3.6    val content: span -> Token.T list
     3.7 -  val resolve_files: Keyword.keywords ->
     3.8 -    (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span
     3.9  end;
    3.10  
    3.11  structure Command_Span: COMMAND_SPAN =
    3.12 @@ -23,47 +21,4 @@
    3.13  fun kind (Span (k, _)) = k;
    3.14  fun content (Span (_, toks)) = toks;
    3.15  
    3.16 -
    3.17 -(* resolve inlined files *)
    3.18 -
    3.19 -local
    3.20 -
    3.21 -fun clean ((t1, i1) :: (t2, i2) :: rest) =
    3.22 -      if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean rest
    3.23 -      else (t1, i1) :: clean ((t2, i2) :: rest)
    3.24 -  | clean toks = toks;
    3.25 -
    3.26 -fun clean_tokens tokens =
    3.27 -  clean (filter (fn (t, _) => Token.is_proper t) (tokens ~~ (0 upto length tokens - 1)));
    3.28 -
    3.29 -fun find_file ((tok, _) :: toks) =
    3.30 -      if Token.is_command tok then
    3.31 -        toks |> get_first (fn (t, i) =>
    3.32 -          if Token.is_name t then
    3.33 -            SOME ((Path.explode (Token.content_of t), Token.pos_of t), i)
    3.34 -              handle ERROR msg => error (msg ^ Position.here (Token.pos_of t))
    3.35 -          else NONE)
    3.36 -      else NONE
    3.37 -  | find_file [] = NONE;
    3.38 -
    3.39 -in
    3.40 -
    3.41 -fun resolve_files keywords read_files span =
    3.42 -  (case span of
    3.43 -    Span (Command_Span (cmd, pos), toks) =>
    3.44 -      if Keyword.is_theory_load keywords cmd then
    3.45 -        (case find_file (clean_tokens toks) of
    3.46 -          NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
    3.47 -        | SOME (path, i) =>
    3.48 -            let
    3.49 -              val toks' = toks |> map_index (fn (j, tok) =>
    3.50 -                if i = j then Token.put_files (read_files cmd path) tok
    3.51 -                else tok);
    3.52 -            in Span (Command_Span (cmd, pos), toks') end)
    3.53 -      else span
    3.54 -  | _ => span);
    3.55 -
    3.56  end;
    3.57 -
    3.58 -end;
    3.59 -
     4.1 --- a/src/Pure/PIDE/command_span.scala	Fri Mar 13 12:44:16 2015 +0100
     4.2 +++ b/src/Pure/PIDE/command_span.scala	Fri Mar 13 12:58:49 2015 +0100
     4.3 @@ -52,64 +52,4 @@
     4.4  
     4.5    def unparsed(source: String): Span =
     4.6      Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
     4.7 -
     4.8 -
     4.9 -  /* resolve inlined files */
    4.10 -
    4.11 -  private def clean_tokens(tokens: List[Token]): List[(Token, Int)] =
    4.12 -  {
    4.13 -    def clean(toks: List[(Token, Int)]): List[(Token, Int)] =
    4.14 -      toks match {
    4.15 -        case (t1, i1) :: (t2, i2) :: rest =>
    4.16 -          if (t1.is_keyword && (t1.source == "%" || t1.source == "--")) clean(rest)
    4.17 -          else (t1, i1) :: clean((t2, i2) :: rest)
    4.18 -        case _ => toks
    4.19 -      }
    4.20 -    clean(tokens.zipWithIndex.filter({ case (t, _) => t.is_proper }))
    4.21 -  }
    4.22 -
    4.23 -  private def find_file(tokens: List[(Token, Int)]): Option[(String, Int)] =
    4.24 -    tokens match {
    4.25 -      case (tok, _) :: toks =>
    4.26 -        if (tok.is_command)
    4.27 -          toks.collectFirst({ case (t, i) if t.is_name => (t.content, i) })
    4.28 -        else None
    4.29 -      case Nil => None
    4.30 -    }
    4.31 -
    4.32 -  def span_files(syntax: Prover.Syntax, span: Span): (List[String], Int) =
    4.33 -    span.kind match {
    4.34 -      case Command_Span(name, _) =>
    4.35 -        syntax.load_command(name) match {
    4.36 -          case Some(exts) =>
    4.37 -            find_file(clean_tokens(span.content)) match {
    4.38 -              case Some((file, i)) =>
    4.39 -                if (exts.isEmpty) (List(file), i)
    4.40 -                else (exts.map(ext => file + "." + ext), i)
    4.41 -              case None => (Nil, -1)
    4.42 -            }
    4.43 -          case None => (Nil, -1)
    4.44 -        }
    4.45 -      case _ => (Nil, -1)
    4.46 -    }
    4.47 -
    4.48 -  def resolve_files(
    4.49 -      resources: Resources,
    4.50 -      syntax: Prover.Syntax,
    4.51 -      node_name: Document.Node.Name,
    4.52 -      span: Span,
    4.53 -      get_blob: Document.Node.Name => Option[Document.Blob])
    4.54 -    : (List[Command.Blob], Int) =
    4.55 -  {
    4.56 -    val (files, index) = span_files(syntax, span)
    4.57 -    val blobs =
    4.58 -      files.map(file =>
    4.59 -        Exn.capture {
    4.60 -          val name =
    4.61 -            Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file)))
    4.62 -          val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
    4.63 -          (name, blob)
    4.64 -        })
    4.65 -    (blobs, index)
    4.66 -  }
    4.67  }
     5.1 --- a/src/Pure/PIDE/document.ML	Fri Mar 13 12:44:16 2015 +0100
     5.2 +++ b/src/Pure/PIDE/document.ML	Fri Mar 13 12:58:49 2015 +0100
     5.3 @@ -307,8 +307,8 @@
     5.4  abstype state = State of
     5.5   {versions: version Inttab.table,  (*version id -> document content*)
     5.6    blobs: (SHA1.digest * string list) Symtab.table,  (*raw digest -> digest, lines*)
     5.7 -  commands: (string * blob_digest list * Token.T list lazy) Inttab.table,
     5.8 -    (*command id -> name, inlined files, command span*)
     5.9 +  commands: (string * blob_digest list * int * Token.T list lazy) Inttab.table,
    5.10 +    (*command id -> name, inlined files, token index of files, command span*)
    5.11    execution: execution}  (*current execution process*)
    5.12  with
    5.13  
    5.14 @@ -385,7 +385,7 @@
    5.15                    else ();
    5.16                in tokens end) ());
    5.17        val commands' =
    5.18 -        Inttab.update_new (command_id, (name, command_blobs, span)) commands
    5.19 +        Inttab.update_new (command_id, (name, command_blobs, blobs_index, span)) commands
    5.20            handle Inttab.DUP dup => err_dup "command" dup;
    5.21        val _ =
    5.22          Position.setmp_thread_data (Position.id_only id)
    5.23 @@ -419,7 +419,7 @@
    5.24                SOME o Inttab.insert (K true) (command_id, the_command state command_id))));
    5.25      val blobs' =
    5.26        (commands', Symtab.empty) |->
    5.27 -        Inttab.fold (fn (_, (_, blobs, _)) => blobs |>
    5.28 +        Inttab.fold (fn (_, (_, blobs, _, _)) => blobs |>
    5.29            fold (fn Exn.Res (_, SOME b) => Symtab.update (b, the_blob state b) | _ => I));
    5.30  
    5.31    in (versions', blobs', commands', execution) end);
    5.32 @@ -585,13 +585,13 @@
    5.33  
    5.34        val command_visible = visible_command node command_id';
    5.35        val command_overlays = overlays node command_id';
    5.36 -      val (command_name, blob_digests, span0) = the_command state command_id';
    5.37 +      val (command_name, blob_digests, blobs_index, span0) = the_command state command_id';
    5.38        val blobs = map (resolve_blob state) blob_digests;
    5.39        val span = Lazy.force span0;
    5.40  
    5.41        val eval' =
    5.42          Command.eval keywords (master_directory node)
    5.43 -          (fn () => the_default illegal_init init span) blobs span eval;
    5.44 +          (fn () => the_default illegal_init init span) (blobs, blobs_index) span eval;
    5.45        val prints' =
    5.46          perhaps (Command.print command_visible command_overlays keywords command_name eval') [];
    5.47        val exec' = (eval', prints');
     6.1 --- a/src/Pure/PIDE/resources.ML	Fri Mar 13 12:44:16 2015 +0100
     6.2 +++ b/src/Pure/PIDE/resources.ML	Fri Mar 13 12:58:49 2015 +0100
     6.3 @@ -128,7 +128,7 @@
     6.4    let
     6.5      fun prepare_span st span =
     6.6        Command_Span.content span
     6.7 -      |> Command.read keywords (Command.read_thy st) master_dir init []
     6.8 +      |> Command.read keywords (Command.read_thy st) master_dir init ([], ~1)
     6.9        |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
    6.10  
    6.11      fun element_result span_elem (st, _) =
     7.1 --- a/src/Pure/PIDE/resources.scala	Fri Mar 13 12:44:16 2015 +0100
     7.2 +++ b/src/Pure/PIDE/resources.scala	Fri Mar 13 12:58:49 2015 +0100
     7.3 @@ -57,7 +57,7 @@
     7.4    def loaded_files(syntax: Prover.Syntax, text: String): List[String] =
     7.5      if (syntax.load_commands_in(text)) {
     7.6        val spans = syntax.parse_spans(text)
     7.7 -      spans.iterator.map(Command_Span.span_files(syntax, _)._1).flatten.toList
     7.8 +      spans.iterator.map(Command.span_files(syntax, _)._1).flatten.toList
     7.9      }
    7.10      else Nil
    7.11  
     8.1 --- a/src/Pure/Thy/thy_syntax.scala	Fri Mar 13 12:44:16 2015 +0100
     8.2 +++ b/src/Pure/Thy/thy_syntax.scala	Fri Mar 13 12:58:49 2015 +0100
     8.3 @@ -164,7 +164,7 @@
     8.4      val cmds0 = commands.iterator(first, last).toList
     8.5      val blobs_spans0 =
     8.6        syntax.parse_spans(cmds0.iterator.map(_.source).mkString).
     8.7 -        map(span => (Command_Span.resolve_files(resources, syntax, name, span, get_blob), span))
     8.8 +        map(span => (Command.resolve_files(resources, syntax, name, span, get_blob), span))
     8.9  
    8.10      val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)
    8.11