separate module Command_Span: mostly syntactic representation;
authorwenzelm
Tue Aug 12 00:08:32 2014 +0200 (2014-08-12 ago)
changeset 57905c0c5652e796e
parent 57904 922273b7bf8a
child 57906 020df63dd0a9
separate module Command_Span: mostly syntactic representation;
potentially prover-specific Output_Syntax.parse_spans;
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/outer_syntax.scala
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/prover.scala
src/Pure/PIDE/resources.ML
src/Pure/PIDE/resources.scala
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/Thy/thy_structure.scala
src/Pure/Thy/thy_syntax.ML
src/Pure/Thy/thy_syntax.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Aug 11 22:59:38 2014 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Aug 12 00:08:32 2014 +0200
     1.3 @@ -33,6 +33,8 @@
     1.4    val print_outer_syntax: unit -> unit
     1.5    val scan: Position.T -> string -> Token.T list
     1.6    val parse: Position.T -> string -> Toplevel.transition list
     1.7 +  val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
     1.8 +  val parse_spans: Token.T list -> Command_Span.span list
     1.9    type isar
    1.10    val isar: TextIO.instream -> bool -> isar
    1.11    val side_comments: Token.T list -> Token.T list
    1.12 @@ -269,6 +271,43 @@
    1.13    |> toplevel_source false NONE lookup_commands_dynamic
    1.14    |> Source.exhaust;
    1.15  
    1.16 +fun parse_tokens lexs pos =
    1.17 +  Source.of_string #>
    1.18 +  Symbol.source #>
    1.19 +  Token.source {do_recover = SOME false} (K lexs) pos #>
    1.20 +  Source.exhaust;
    1.21 +
    1.22 +
    1.23 +(* parse spans *)
    1.24 +
    1.25 +local
    1.26 +
    1.27 +fun ship span =
    1.28 +  let
    1.29 +    val kind =
    1.30 +      if not (null span) andalso Token.is_command (hd span) andalso not (exists Token.is_error span)
    1.31 +      then Command_Span.Command_Span (Token.content_of (hd span), Token.pos_of (hd span))
    1.32 +      else if forall Token.is_improper span then Command_Span.Ignored_Span
    1.33 +      else Command_Span.Malformed_Span;
    1.34 +  in cons (Command_Span.Span (kind, span)) end;
    1.35 +
    1.36 +fun flush (result, content, improper) =
    1.37 +  result
    1.38 +  |> not (null content) ? ship (rev content)
    1.39 +  |> not (null improper) ? ship (rev improper);
    1.40 +
    1.41 +fun parse tok (result, content, improper) =
    1.42 +  if Token.is_command tok then (flush (result, content, improper), [tok], [])
    1.43 +  else if Token.is_improper tok then (result, content, tok :: improper)
    1.44 +  else (result, tok :: (improper @ content), []);
    1.45 +
    1.46 +in
    1.47 +
    1.48 +fun parse_spans toks =
    1.49 +  fold parse toks ([], [], []) |> flush |> rev;
    1.50 +
    1.51 +end;
    1.52 +
    1.53  
    1.54  (* interactive source of toplevel transformers *)
    1.55  
     2.1 --- a/src/Pure/Isar/outer_syntax.scala	Mon Aug 11 22:59:38 2014 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 12 00:08:32 2014 +0200
     2.3 @@ -152,6 +152,41 @@
     2.4    }
     2.5  
     2.6  
     2.7 +  /* parse_spans */
     2.8 +
     2.9 +  def parse_spans(toks: List[Token]): List[Command_Span.Span] =
    2.10 +  {
    2.11 +    val result = new mutable.ListBuffer[Command_Span.Span]
    2.12 +    val content = new mutable.ListBuffer[Token]
    2.13 +    val improper = new mutable.ListBuffer[Token]
    2.14 +
    2.15 +    def ship(span: List[Token])
    2.16 +    {
    2.17 +      val kind =
    2.18 +        if (!span.isEmpty && span.head.is_command && !span.exists(_.is_error))
    2.19 +          Command_Span.Command_Span(span.head.source)
    2.20 +        else if (span.forall(_.is_improper)) Command_Span.Ignored_Span
    2.21 +        else Command_Span.Malformed_Span
    2.22 +      result += Command_Span.Span(kind, span)
    2.23 +    }
    2.24 +
    2.25 +    def flush()
    2.26 +    {
    2.27 +      if (!content.isEmpty) { ship(content.toList); content.clear }
    2.28 +      if (!improper.isEmpty) { ship(improper.toList); improper.clear }
    2.29 +    }
    2.30 +
    2.31 +    for (tok <- toks) {
    2.32 +      if (tok.is_command) { flush(); content += tok }
    2.33 +      else if (tok.is_improper) improper += tok
    2.34 +      else { content ++= improper; improper.clear; content += tok }
    2.35 +    }
    2.36 +    flush()
    2.37 +
    2.38 +    result.toList
    2.39 +  }
    2.40 +
    2.41 +
    2.42    /* language context */
    2.43  
    2.44    def set_language_context(context: Completion.Language_Context): Outer_Syntax =
     3.1 --- a/src/Pure/PIDE/command.ML	Mon Aug 11 22:59:38 2014 +0200
     3.2 +++ b/src/Pure/PIDE/command.ML	Tue Aug 12 00:08:32 2014 +0200
     3.3 @@ -121,9 +121,9 @@
     3.4    in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end
     3.5  
     3.6  fun resolve_files master_dir blobs toks =
     3.7 -  (case Thy_Syntax.parse_spans toks of
     3.8 +  (case Outer_Syntax.parse_spans toks of
     3.9      [span] => span
    3.10 -      |> Thy_Syntax.resolve_files (fn cmd => fn (path, pos) =>
    3.11 +      |> Command_Span.resolve_files (fn cmd => fn (path, pos) =>
    3.12          let
    3.13            fun make_file src_path (Exn.Res (file_node, NONE)) =
    3.14                  Exn.interruptible_capture (fn () =>
    3.15 @@ -140,7 +140,7 @@
    3.16              map2 make_file src_paths blobs
    3.17            else error ("Misalignment of inlined files" ^ Position.here pos)
    3.18          end)
    3.19 -      |> Thy_Syntax.span_content
    3.20 +      |> Command_Span.content
    3.21    | _ => toks);
    3.22  
    3.23  in
     4.1 --- a/src/Pure/PIDE/command.scala	Mon Aug 11 22:59:38 2014 +0200
     4.2 +++ b/src/Pure/PIDE/command.scala	Tue Aug 12 00:08:32 2014 +0200
     4.3 @@ -254,14 +254,14 @@
     4.4      id: Document_ID.Command,
     4.5      node_name: Document.Node.Name,
     4.6      blobs: List[Blob],
     4.7 -    span: Thy_Syntax.Span): Command =
     4.8 +    span: Command_Span.Span): Command =
     4.9    {
    4.10      val (source, span1) = span.compact_source
    4.11      new Command(id, node_name, blobs, span1, source, Results.empty, Markup_Tree.empty)
    4.12    }
    4.13  
    4.14    val empty: Command =
    4.15 -    Command(Document_ID.none, Document.Node.Name.empty, Nil, Thy_Syntax.empty_span)
    4.16 +    Command(Document_ID.none, Document.Node.Name.empty, Nil, Command_Span.empty)
    4.17  
    4.18    def unparsed(
    4.19      id: Document_ID.Command,
    4.20 @@ -269,7 +269,7 @@
    4.21      results: Results,
    4.22      markup: Markup_Tree): Command =
    4.23    {
    4.24 -    val (source1, span1) = Thy_Syntax.unparsed_span(source).compact_source
    4.25 +    val (source1, span1) = Command_Span.unparsed(source).compact_source
    4.26      new Command(id, Document.Node.Name.empty, Nil, span1, source1, results, markup)
    4.27    }
    4.28  
    4.29 @@ -312,7 +312,7 @@
    4.30      val id: Document_ID.Command,
    4.31      val node_name: Document.Node.Name,
    4.32      val blobs: List[Command.Blob],
    4.33 -    val span: Thy_Syntax.Span,
    4.34 +    val span: Command_Span.Span,
    4.35      val source: String,
    4.36      val init_results: Command.Results,
    4.37      val init_markup: Markup_Tree)
    4.38 @@ -320,12 +320,12 @@
    4.39    /* name and classification */
    4.40  
    4.41    def name: String =
    4.42 -    span.kind match { case Thy_Syntax.Command_Span(name) => name case _ => "" }
    4.43 +    span.kind match { case Command_Span.Command_Span(name) => name case _ => "" }
    4.44  
    4.45    override def toString = id + "/" + span.kind.toString
    4.46  
    4.47 -  def is_proper: Boolean = span.kind.isInstanceOf[Thy_Syntax.Command_Span]
    4.48 -  def is_ignored: Boolean = span.kind == Thy_Syntax.Ignored_Span
    4.49 +  def is_proper: Boolean = span.kind.isInstanceOf[Command_Span.Command_Span]
    4.50 +  def is_ignored: Boolean = span.kind == Command_Span.Ignored_Span
    4.51  
    4.52    def is_undefined: Boolean = id == Document_ID.none
    4.53    val is_unparsed: Boolean = span.content.exists(_.is_unparsed)
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/PIDE/command_span.ML	Tue Aug 12 00:08:32 2014 +0200
     5.3 @@ -0,0 +1,70 @@
     5.4 +(*  Title:      Pure/PIDE/command_span.ML
     5.5 +    Author:     Makarius
     5.6 +
     5.7 +Syntactic representation of command spans.
     5.8 +*)
     5.9 +
    5.10 +signature COMMAND_SPAN =
    5.11 +sig
    5.12 +  datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span
    5.13 +  datatype span = Span of kind * Token.T list
    5.14 +  val kind: span -> kind
    5.15 +  val content: span -> Token.T list
    5.16 +  val resolve_files: (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span
    5.17 +end;
    5.18 +
    5.19 +structure Command_Span: COMMAND_SPAN =
    5.20 +struct
    5.21 +
    5.22 +datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span;
    5.23 +datatype span = Span of kind * Token.T list;
    5.24 +
    5.25 +fun kind (Span (k, _)) = k;
    5.26 +fun content (Span (_, toks)) = toks;
    5.27 +
    5.28 +
    5.29 +(* resolve inlined files *)
    5.30 +
    5.31 +local
    5.32 +
    5.33 +fun clean ((i1, t1) :: (i2, t2) :: toks) =
    5.34 +      if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean toks
    5.35 +      else (i1, t1) :: clean ((i2, t2) :: toks)
    5.36 +  | clean toks = toks;
    5.37 +
    5.38 +fun clean_tokens toks =
    5.39 +  ((0 upto length toks - 1) ~~ toks)
    5.40 +  |> filter (fn (_, tok) => Token.is_proper tok)
    5.41 +  |> clean;
    5.42 +
    5.43 +fun find_file ((_, tok) :: toks) =
    5.44 +      if Token.is_command tok then
    5.45 +        toks |> get_first (fn (i, tok) =>
    5.46 +          if Token.is_name tok then
    5.47 +            SOME (i, (Path.explode (Token.content_of tok), Token.pos_of tok))
    5.48 +              handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok))
    5.49 +          else NONE)
    5.50 +      else NONE
    5.51 +  | find_file [] = NONE;
    5.52 +
    5.53 +in
    5.54 +
    5.55 +fun resolve_files read_files span =
    5.56 +  (case span of
    5.57 +    Span (Command_Span (cmd, pos), toks) =>
    5.58 +      if Keyword.is_theory_load cmd then
    5.59 +        (case find_file (clean_tokens toks) of
    5.60 +          NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
    5.61 +        | SOME (i, path) =>
    5.62 +            let
    5.63 +              val toks' = toks |> map_index (fn (j, tok) =>
    5.64 +                if i = j then Token.put_files (read_files cmd path) tok
    5.65 +                else tok);
    5.66 +            in Span (Command_Span (cmd, pos), toks') end)
    5.67 +      else span
    5.68 +  | _ => span);
    5.69 +
    5.70 +end;
    5.71 +
    5.72 +end;
    5.73 +
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Pure/PIDE/command_span.scala	Tue Aug 12 00:08:32 2014 +0200
     6.3 @@ -0,0 +1,104 @@
     6.4 +/*  Title:      Pure/PIDE/command_span.scala
     6.5 +    Author:     Makarius
     6.6 +
     6.7 +Syntactic representation of command spans.
     6.8 +*/
     6.9 +
    6.10 +package isabelle
    6.11 +
    6.12 +
    6.13 +import scala.collection.mutable
    6.14 +
    6.15 +
    6.16 +object Command_Span
    6.17 +{
    6.18 +  sealed abstract class Kind {
    6.19 +    override def toString: String =
    6.20 +      this match {
    6.21 +        case Command_Span(name) => if (name != "") name else "<command>"
    6.22 +        case Ignored_Span => "<ignored>"
    6.23 +        case Malformed_Span => "<malformed>"
    6.24 +      }
    6.25 +  }
    6.26 +  case class Command_Span(name: String) extends Kind
    6.27 +  case object Ignored_Span extends Kind
    6.28 +  case object Malformed_Span extends Kind
    6.29 +
    6.30 +  sealed case class Span(kind: Kind, content: List[Token])
    6.31 +  {
    6.32 +    def compact_source: (String, Span) =
    6.33 +    {
    6.34 +      val source: String =
    6.35 +        content match {
    6.36 +          case List(tok) => tok.source
    6.37 +          case toks => toks.map(_.source).mkString
    6.38 +        }
    6.39 +
    6.40 +      val content1 = new mutable.ListBuffer[Token]
    6.41 +      var i = 0
    6.42 +      for (Token(kind, s) <- content) {
    6.43 +        val n = s.length
    6.44 +        val s1 = source.substring(i, i + n)
    6.45 +        content1 += Token(kind, s1)
    6.46 +        i += n
    6.47 +      }
    6.48 +      (source, Span(kind, content1.toList))
    6.49 +    }
    6.50 +  }
    6.51 +
    6.52 +  val empty: Span = Span(Ignored_Span, Nil)
    6.53 +
    6.54 +  def unparsed(source: String): Span =
    6.55 +    Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
    6.56 +
    6.57 +
    6.58 +  /* resolve inlined files */
    6.59 +
    6.60 +  private def find_file(tokens: List[Token]): Option[String] =
    6.61 +  {
    6.62 +    def clean(toks: List[Token]): List[Token] =
    6.63 +      toks match {
    6.64 +        case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
    6.65 +        case t :: ts => t :: clean(ts)
    6.66 +        case Nil => Nil
    6.67 +      }
    6.68 +    clean(tokens.filter(_.is_proper)) match {
    6.69 +      case tok :: toks if tok.is_command => toks.find(_.is_name).map(_.content)
    6.70 +      case _ => None
    6.71 +    }
    6.72 +  }
    6.73 +
    6.74 +  def span_files(syntax: Prover.Syntax, span: Span): List[String] =
    6.75 +    span.kind match {
    6.76 +      case Command_Span(name) =>
    6.77 +        syntax.load_command(name) match {
    6.78 +          case Some(exts) =>
    6.79 +            find_file(span.content) match {
    6.80 +              case Some(file) =>
    6.81 +                if (exts.isEmpty) List(file)
    6.82 +                else exts.map(ext => file + "." + ext)
    6.83 +              case None => Nil
    6.84 +            }
    6.85 +          case None => Nil
    6.86 +        }
    6.87 +      case _ => Nil
    6.88 +    }
    6.89 +
    6.90 +  def resolve_files(
    6.91 +      resources: Resources,
    6.92 +      syntax: Prover.Syntax,
    6.93 +      node_name: Document.Node.Name,
    6.94 +      span: Span,
    6.95 +      get_blob: Document.Node.Name => Option[Document.Blob])
    6.96 +    : List[Command.Blob] =
    6.97 +  {
    6.98 +    span_files(syntax, span).map(file_name =>
    6.99 +      Exn.capture {
   6.100 +        val name =
   6.101 +          Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
   6.102 +        val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
   6.103 +        (name, blob)
   6.104 +      })
   6.105 +  }
   6.106 +}
   6.107 +
     7.1 --- a/src/Pure/PIDE/document.ML	Mon Aug 11 22:59:38 2014 +0200
     7.2 +++ b/src/Pure/PIDE/document.ML	Tue Aug 12 00:08:32 2014 +0200
     7.3 @@ -318,7 +318,7 @@
     7.4        val span =
     7.5          Lazy.lazy (fn () =>
     7.6            Position.setmp_thread_data (Position.id_only id)
     7.7 -            (fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id) text) ());
     7.8 +            (fn () => Outer_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id) text) ());
     7.9        val _ =
    7.10          Position.setmp_thread_data (Position.id_only id)
    7.11            (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
     8.1 --- a/src/Pure/PIDE/prover.scala	Mon Aug 11 22:59:38 2014 +0200
     8.2 +++ b/src/Pure/PIDE/prover.scala	Tue Aug 12 00:08:32 2014 +0200
     8.3 @@ -15,6 +15,7 @@
     8.4    {
     8.5      def add_keywords(keywords: Thy_Header.Keywords): Syntax
     8.6      def scan(input: CharSequence): List[Token]
     8.7 +    def parse_spans(toks: List[Token]): List[Command_Span.Span]
     8.8      def load_command(name: String): Option[List[String]]
     8.9      def load_commands_in(text: String): Boolean
    8.10    }
     9.1 --- a/src/Pure/PIDE/resources.ML	Mon Aug 11 22:59:38 2014 +0200
     9.2 +++ b/src/Pure/PIDE/resources.ML	Tue Aug 12 00:08:32 2014 +0200
     9.3 @@ -132,7 +132,7 @@
     9.4  fun excursion master_dir last_timing init elements =
     9.5    let
     9.6      fun prepare_span span =
     9.7 -      Thy_Syntax.span_content span
     9.8 +      Command_Span.content span
     9.9        |> Command.read init master_dir []
    9.10        |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
    9.11  
    9.12 @@ -157,8 +157,8 @@
    9.13      val _ = Thy_Header.define_keywords header;
    9.14  
    9.15      val lexs = Keyword.get_lexicons ();
    9.16 -    val toks = Thy_Syntax.parse_tokens lexs text_pos text;
    9.17 -    val spans = Thy_Syntax.parse_spans toks;
    9.18 +    val toks = Outer_Syntax.parse_tokens lexs text_pos text;
    9.19 +    val spans = Outer_Syntax.parse_spans toks;
    9.20      val elements = Thy_Syntax.parse_elements spans;
    9.21  
    9.22      fun init () =
    10.1 --- a/src/Pure/PIDE/resources.scala	Mon Aug 11 22:59:38 2014 +0200
    10.2 +++ b/src/Pure/PIDE/resources.scala	Tue Aug 12 00:08:32 2014 +0200
    10.3 @@ -56,8 +56,8 @@
    10.4  
    10.5    def loaded_files(syntax: Prover.Syntax, text: String): List[String] =
    10.6      if (syntax.load_commands_in(text)) {
    10.7 -      val spans = Thy_Syntax.parse_spans(syntax.scan(text))
    10.8 -      spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList
    10.9 +      val spans = syntax.parse_spans(syntax.scan(text))
   10.10 +      spans.iterator.map(Command_Span.span_files(syntax, _)).flatten.toList
   10.11      }
   10.12      else Nil
   10.13  
    11.1 --- a/src/Pure/ROOT	Mon Aug 11 22:59:38 2014 +0200
    11.2 +++ b/src/Pure/ROOT	Tue Aug 12 00:08:32 2014 +0200
    11.3 @@ -160,6 +160,7 @@
    11.4      "ML/ml_syntax.ML"
    11.5      "PIDE/active.ML"
    11.6      "PIDE/command.ML"
    11.7 +    "PIDE/command_span.ML"
    11.8      "PIDE/document.ML"
    11.9      "PIDE/document_id.ML"
   11.10      "PIDE/execution.ML"
    12.1 --- a/src/Pure/ROOT.ML	Mon Aug 11 22:59:38 2014 +0200
    12.2 +++ b/src/Pure/ROOT.ML	Tue Aug 12 00:08:32 2014 +0200
    12.3 @@ -236,6 +236,7 @@
    12.4  
    12.5  (*theory sources*)
    12.6  use "Thy/thy_header.ML";
    12.7 +use "PIDE/command_span.ML";
    12.8  use "Thy/thy_syntax.ML";
    12.9  use "Thy/html.ML";
   12.10  use "Thy/latex.ML";
    13.1 --- a/src/Pure/Thy/thy_structure.scala	Mon Aug 11 22:59:38 2014 +0200
    13.2 +++ b/src/Pure/Thy/thy_structure.scala	Tue Aug 12 00:08:32 2014 +0200
    13.3 @@ -63,7 +63,7 @@
    13.4  
    13.5      /* result structure */
    13.6  
    13.7 -    val spans = Thy_Syntax.parse_spans(syntax.scan(text))
    13.8 +    val spans = syntax.parse_spans(syntax.scan(text))
    13.9      spans.foreach(span => add(Command(Document_ID.none, node_name, Nil, span)))
   13.10      result()
   13.11    }
    14.1 --- a/src/Pure/Thy/thy_syntax.ML	Mon Aug 11 22:59:38 2014 +0200
    14.2 +++ b/src/Pure/Thy/thy_syntax.ML	Tue Aug 12 00:08:32 2014 +0200
    14.3 @@ -6,39 +6,21 @@
    14.4  
    14.5  signature THY_SYNTAX =
    14.6  sig
    14.7 -  val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
    14.8    val reports_of_tokens: Token.T list -> bool * Position.report_text list
    14.9    val present_token: Token.T -> Output.output
   14.10 -  datatype span_kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span
   14.11 -  datatype span = Span of span_kind * Token.T list
   14.12 -  val span_kind: span -> span_kind
   14.13 -  val span_content: span -> Token.T list
   14.14 -  val present_span: span -> Output.output
   14.15 -  val parse_spans: Token.T list -> span list
   14.16 -  val resolve_files: (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span
   14.17 +  val present_span: Command_Span.span -> Output.output
   14.18    datatype 'a element = Element of 'a * ('a element list * 'a) option
   14.19    val atom: 'a -> 'a element
   14.20    val map_element: ('a -> 'b) -> 'a element -> 'b element
   14.21    val flat_element: 'a element -> 'a list
   14.22    val last_element: 'a element -> 'a
   14.23 -  val parse_elements: span list -> span element list
   14.24 +  val parse_elements: Command_Span.span list -> Command_Span.span element list
   14.25  end;
   14.26  
   14.27  structure Thy_Syntax: THY_SYNTAX =
   14.28  struct
   14.29  
   14.30 -(** tokens **)
   14.31 -
   14.32 -(* parse *)
   14.33 -
   14.34 -fun parse_tokens lexs pos =
   14.35 -  Source.of_string #>
   14.36 -  Symbol.source #>
   14.37 -  Token.source {do_recover = SOME false} (K lexs) pos #>
   14.38 -  Source.exhaust;
   14.39 -
   14.40 -
   14.41 -(* present *)
   14.42 +(** presentation **)
   14.43  
   14.44  local
   14.45  
   14.46 @@ -60,97 +42,12 @@
   14.47    let val results = map reports_of_token toks
   14.48    in (exists fst results, maps snd results) end;
   14.49  
   14.50 +end;
   14.51 +
   14.52  fun present_token tok =
   14.53    Markup.enclose (Token.markup tok) (Output.output (Token.unparse tok));
   14.54  
   14.55 -end;
   14.56 -
   14.57 -
   14.58 -
   14.59 -(** spans **)
   14.60 -
   14.61 -datatype span_kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span;
   14.62 -datatype span = Span of span_kind * Token.T list;
   14.63 -
   14.64 -fun span_kind (Span (k, _)) = k;
   14.65 -fun span_content (Span (_, toks)) = toks;
   14.66 -
   14.67 -val present_span = implode o map present_token o span_content;
   14.68 -
   14.69 -
   14.70 -(* parse *)
   14.71 -
   14.72 -local
   14.73 -
   14.74 -fun ship span =
   14.75 -  let
   14.76 -    val kind =
   14.77 -      if not (null span) andalso Token.is_command (hd span) andalso not (exists Token.is_error span)
   14.78 -      then Command_Span (Token.content_of (hd span), Token.pos_of (hd span))
   14.79 -      else if forall Token.is_improper span then Ignored_Span
   14.80 -      else Malformed_Span;
   14.81 -  in cons (Span (kind, span)) end;
   14.82 -
   14.83 -fun flush (result, content, improper) =
   14.84 -  result
   14.85 -  |> not (null content) ? ship (rev content)
   14.86 -  |> not (null improper) ? ship (rev improper);
   14.87 -
   14.88 -fun parse tok (result, content, improper) =
   14.89 -  if Token.is_command tok then (flush (result, content, improper), [tok], [])
   14.90 -  else if Token.is_improper tok then (result, content, tok :: improper)
   14.91 -  else (result, tok :: (improper @ content), []);
   14.92 -
   14.93 -in
   14.94 -
   14.95 -fun parse_spans toks =
   14.96 -  fold parse toks ([], [], []) |> flush |> rev;
   14.97 -
   14.98 -end;
   14.99 -
  14.100 -
  14.101 -(* inlined files *)
  14.102 -
  14.103 -local
  14.104 -
  14.105 -fun clean ((i1, t1) :: (i2, t2) :: toks) =
  14.106 -      if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean toks
  14.107 -      else (i1, t1) :: clean ((i2, t2) :: toks)
  14.108 -  | clean toks = toks;
  14.109 -
  14.110 -fun clean_tokens toks =
  14.111 -  ((0 upto length toks - 1) ~~ toks)
  14.112 -  |> filter (fn (_, tok) => Token.is_proper tok)
  14.113 -  |> clean;
  14.114 -
  14.115 -fun find_file ((_, tok) :: toks) =
  14.116 -      if Token.is_command tok then
  14.117 -        toks |> get_first (fn (i, tok) =>
  14.118 -          if Token.is_name tok then
  14.119 -            SOME (i, (Path.explode (Token.content_of tok), Token.pos_of tok))
  14.120 -              handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok))
  14.121 -          else NONE)
  14.122 -      else NONE
  14.123 -  | find_file [] = NONE;
  14.124 -
  14.125 -in
  14.126 -
  14.127 -fun resolve_files read_files span =
  14.128 -  (case span of
  14.129 -    Span (Command_Span (cmd, pos), toks) =>
  14.130 -      if Keyword.is_theory_load cmd then
  14.131 -        (case find_file (clean_tokens toks) of
  14.132 -          NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
  14.133 -        | SOME (i, path) =>
  14.134 -            let
  14.135 -              val toks' = toks |> map_index (fn (j, tok) =>
  14.136 -                if i = j then Token.put_files (read_files cmd path) tok
  14.137 -                else tok);
  14.138 -            in Span (Command_Span (cmd, pos), toks') end)
  14.139 -      else span
  14.140 -  | _ => span);
  14.141 -
  14.142 -end;
  14.143 +val present_span = implode o map present_token o Command_Span.content;
  14.144  
  14.145  
  14.146  
  14.147 @@ -174,9 +71,9 @@
  14.148  
  14.149  (* scanning spans *)
  14.150  
  14.151 -val eof = Span (Command_Span ("", Position.none), []);
  14.152 +val eof = Command_Span.Span (Command_Span.Command_Span ("", Position.none), []);
  14.153  
  14.154 -fun is_eof (Span (Command_Span ("", _), _)) = true
  14.155 +fun is_eof (Command_Span.Span (Command_Span.Command_Span ("", _), _)) = true
  14.156    | is_eof _ = false;
  14.157  
  14.158  val not_eof = not o is_eof;
  14.159 @@ -189,10 +86,13 @@
  14.160  local
  14.161  
  14.162  fun command_with pred =
  14.163 -  Scan.one (fn (Span (Command_Span (name, _), _)) => pred name | _ => false);
  14.164 +  Scan.one
  14.165 +    (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) => pred name | _ => false);
  14.166  
  14.167  val proof_atom =
  14.168 -  Scan.one (fn (Span (Command_Span (name, _), _)) => Keyword.is_proof_body name | _ => true) >> atom;
  14.169 +  Scan.one
  14.170 +    (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) => Keyword.is_proof_body name
  14.171 +      | _ => true) >> atom;
  14.172  
  14.173  fun proof_element x = (command_with Keyword.is_proof_goal -- proof_rest >> element || proof_atom) x
  14.174  and proof_rest x = (Scan.repeat proof_element -- command_with Keyword.is_qed) x;
    15.1 --- a/src/Pure/Thy/thy_syntax.scala	Mon Aug 11 22:59:38 2014 +0200
    15.2 +++ b/src/Pure/Thy/thy_syntax.scala	Tue Aug 12 00:08:32 2014 +0200
    15.3 @@ -13,84 +13,6 @@
    15.4  
    15.5  object Thy_Syntax
    15.6  {
    15.7 -  /** spans **/
    15.8 -
    15.9 -  sealed abstract class Span_Kind {
   15.10 -    override def toString: String =
   15.11 -      this match {
   15.12 -        case Command_Span(name) => if (name != "") name else "<command>"
   15.13 -        case Ignored_Span => "<ignored>"
   15.14 -        case Malformed_Span => "<malformed>"
   15.15 -      }
   15.16 -  }
   15.17 -  case class Command_Span(name: String) extends Span_Kind
   15.18 -  case object Ignored_Span extends Span_Kind
   15.19 -  case object Malformed_Span extends Span_Kind
   15.20 -
   15.21 -  sealed case class Span(kind: Span_Kind, content: List[Token])
   15.22 -  {
   15.23 -    def compact_source: (String, Span) =
   15.24 -    {
   15.25 -      val source: String =
   15.26 -        content match {
   15.27 -          case List(tok) => tok.source
   15.28 -          case toks => toks.map(_.source).mkString
   15.29 -        }
   15.30 -
   15.31 -      val content1 = new mutable.ListBuffer[Token]
   15.32 -      var i = 0
   15.33 -      for (Token(kind, s) <- content) {
   15.34 -        val n = s.length
   15.35 -        val s1 = source.substring(i, i + n)
   15.36 -        content1 += Token(kind, s1)
   15.37 -        i += n
   15.38 -      }
   15.39 -      (source, Span(kind, content1.toList))
   15.40 -    }
   15.41 -  }
   15.42 -
   15.43 -  val empty_span: Span = Span(Ignored_Span, Nil)
   15.44 -
   15.45 -  def unparsed_span(source: String): Span =
   15.46 -    Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
   15.47 -
   15.48 -
   15.49 -  /* parse */
   15.50 -
   15.51 -  def parse_spans(toks: List[Token]): List[Span] =
   15.52 -  {
   15.53 -    val result = new mutable.ListBuffer[Span]
   15.54 -    val content = new mutable.ListBuffer[Token]
   15.55 -    val improper = new mutable.ListBuffer[Token]
   15.56 -
   15.57 -    def ship(span: List[Token])
   15.58 -    {
   15.59 -      val kind =
   15.60 -        if (!span.isEmpty && span.head.is_command && !span.exists(_.is_error))
   15.61 -          Command_Span(span.head.source)
   15.62 -        else if (span.forall(_.is_improper)) Ignored_Span
   15.63 -        else Malformed_Span
   15.64 -      result += Span(kind, span)
   15.65 -    }
   15.66 -
   15.67 -    def flush()
   15.68 -    {
   15.69 -      if (!content.isEmpty) { ship(content.toList); content.clear }
   15.70 -      if (!improper.isEmpty) { ship(improper.toList); improper.clear }
   15.71 -    }
   15.72 -
   15.73 -    for (tok <- toks) {
   15.74 -      if (tok.is_command) { flush(); content += tok }
   15.75 -      else if (tok.is_improper) improper += tok
   15.76 -      else { content ++= improper; improper.clear; content += tok }
   15.77 -    }
   15.78 -    flush()
   15.79 -
   15.80 -    result.toList
   15.81 -  }
   15.82 -
   15.83 -
   15.84 -
   15.85    /** perspective **/
   15.86  
   15.87    def command_perspective(
   15.88 @@ -222,62 +144,12 @@
   15.89    }
   15.90  
   15.91  
   15.92 -  /* inlined files */
   15.93 -
   15.94 -  private def find_file(tokens: List[Token]): Option[String] =
   15.95 -  {
   15.96 -    def clean(toks: List[Token]): List[Token] =
   15.97 -      toks match {
   15.98 -        case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
   15.99 -        case t :: ts => t :: clean(ts)
  15.100 -        case Nil => Nil
  15.101 -      }
  15.102 -    clean(tokens.filter(_.is_proper)) match {
  15.103 -      case tok :: toks if tok.is_command => toks.find(_.is_name).map(_.content)
  15.104 -      case _ => None
  15.105 -    }
  15.106 -  }
  15.107 -
  15.108 -  def span_files(syntax: Prover.Syntax, span: Span): List[String] =
  15.109 -    span.kind match {
  15.110 -      case Command_Span(name) =>
  15.111 -        syntax.load_command(name) match {
  15.112 -          case Some(exts) =>
  15.113 -            find_file(span.content) match {
  15.114 -              case Some(file) =>
  15.115 -                if (exts.isEmpty) List(file)
  15.116 -                else exts.map(ext => file + "." + ext)
  15.117 -              case None => Nil
  15.118 -            }
  15.119 -          case None => Nil
  15.120 -        }
  15.121 -      case _ => Nil
  15.122 -    }
  15.123 -
  15.124 -  def resolve_files(
  15.125 -      resources: Resources,
  15.126 -      syntax: Prover.Syntax,
  15.127 -      node_name: Document.Node.Name,
  15.128 -      span: Span,
  15.129 -      get_blob: Document.Node.Name => Option[Document.Blob])
  15.130 -    : List[Command.Blob] =
  15.131 -  {
  15.132 -    span_files(syntax, span).map(file_name =>
  15.133 -      Exn.capture {
  15.134 -        val name =
  15.135 -          Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
  15.136 -        val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
  15.137 -        (name, blob)
  15.138 -      })
  15.139 -  }
  15.140 -
  15.141 -
  15.142    /* reparse range of command spans */
  15.143  
  15.144    @tailrec private def chop_common(
  15.145        cmds: List[Command],
  15.146 -      blobs_spans: List[(List[Command.Blob], Span)])
  15.147 -    : (List[Command], List[(List[Command.Blob], Span)]) =
  15.148 +      blobs_spans: List[(List[Command.Blob], Command_Span.Span)])
  15.149 +    : (List[Command], List[(List[Command.Blob], Command_Span.Span)]) =
  15.150    {
  15.151      (cmds, blobs_spans) match {
  15.152        case (cmd :: cmds, (blobs, span) :: rest) if cmd.blobs == blobs && cmd.span == span =>
  15.153 @@ -296,8 +168,8 @@
  15.154    {
  15.155      val cmds0 = commands.iterator(first, last).toList
  15.156      val blobs_spans0 =
  15.157 -      parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
  15.158 -        map(span => (resolve_files(resources, syntax, name, span, get_blob), span))
  15.159 +      syntax.parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
  15.160 +        map(span => (Command_Span.resolve_files(resources, syntax, name, span, get_blob), span))
  15.161  
  15.162      val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)
  15.163  
    16.1 --- a/src/Pure/build-jars	Mon Aug 11 22:59:38 2014 +0200
    16.2 +++ b/src/Pure/build-jars	Tue Aug 12 00:08:32 2014 +0200
    16.3 @@ -54,6 +54,7 @@
    16.4    Isar/token.scala
    16.5    ML/ml_lex.scala
    16.6    PIDE/command.scala
    16.7 +  PIDE/command_span.scala
    16.8    PIDE/document.scala
    16.9    PIDE/document_id.scala
   16.10    PIDE/editor.scala