more explicit type Span in Scala, according to ML version;
authorwenzelm
Mon Aug 11 22:29:48 2014 +0200 (2014-08-11 ago)
changeset 57901e1abca2527da
parent 57900 fd03765b06c0
child 57902 3f1fd41ee821
more explicit type Span in Scala, according to ML version;
src/Pure/Isar/outer_syntax.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/prover.scala
src/Pure/Thy/thy_syntax.ML
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Mon Aug 11 20:46:56 2014 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Mon Aug 11 22:29:48 2014 +0200
     1.3 @@ -57,8 +57,8 @@
     1.4    def keyword_kind_files(name: String): Option[(String, List[String])] = keywords.get(name)
     1.5    def keyword_kind(name: String): Option[String] = keyword_kind_files(name).map(_._1)
     1.6  
     1.7 -  def load(span: List[Token]): Option[List[String]] =
     1.8 -    keywords.get(Command.name(span)) match {
     1.9 +  def load_command(name: String): Option[List[String]] =
    1.10 +    keywords.get(name) match {
    1.11        case Some((Keyword.THY_LOAD, exts)) => Some(exts)
    1.12        case _ => None
    1.13      }
     2.1 --- a/src/Pure/PIDE/command.scala	Mon Aug 11 20:46:56 2014 +0200
     2.2 +++ b/src/Pure/PIDE/command.scala	Mon Aug 11 22:29:48 2014 +0200
     2.3 @@ -250,39 +250,18 @@
     2.4  
     2.5    /* make commands */
     2.6  
     2.7 -  def name(span: List[Token]): String =
     2.8 -    span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" }
     2.9 -
    2.10 -  private def source_span(span: List[Token]): (String, List[Token]) =
    2.11 -  {
    2.12 -    val source: String =
    2.13 -      span match {
    2.14 -        case List(tok) => tok.source
    2.15 -        case _ => span.map(_.source).mkString
    2.16 -      }
    2.17 -
    2.18 -    val span1 = new mutable.ListBuffer[Token]
    2.19 -    var i = 0
    2.20 -    for (Token(kind, s) <- span) {
    2.21 -      val n = s.length
    2.22 -      val s1 = source.substring(i, i + n)
    2.23 -      span1 += Token(kind, s1)
    2.24 -      i += n
    2.25 -    }
    2.26 -    (source, span1.toList)
    2.27 -  }
    2.28 -
    2.29    def apply(
    2.30      id: Document_ID.Command,
    2.31      node_name: Document.Node.Name,
    2.32      blobs: List[Blob],
    2.33 -    span: List[Token]): Command =
    2.34 +    span: Thy_Syntax.Span): Command =
    2.35    {
    2.36 -    val (source, span1) = source_span(span)
    2.37 +    val (source, span1) = span.compact_source
    2.38      new Command(id, node_name, blobs, span1, source, Results.empty, Markup_Tree.empty)
    2.39    }
    2.40  
    2.41 -  val empty: Command = Command(Document_ID.none, Document.Node.Name.empty, Nil, Nil)
    2.42 +  val empty: Command =
    2.43 +    Command(Document_ID.none, Document.Node.Name.empty, Nil, Thy_Syntax.empty_span)
    2.44  
    2.45    def unparsed(
    2.46      id: Document_ID.Command,
    2.47 @@ -290,8 +269,8 @@
    2.48      results: Results,
    2.49      markup: Markup_Tree): Command =
    2.50    {
    2.51 -    val (source1, span) = source_span(List(Token(Token.Kind.UNPARSED, source)))
    2.52 -    new Command(id, Document.Node.Name.empty, Nil, span, source1, results, markup)
    2.53 +    val (source1, span1) = Thy_Syntax.unparsed_span(source).compact_source
    2.54 +    new Command(id, Document.Node.Name.empty, Nil, span1, source1, results, markup)
    2.55    }
    2.56  
    2.57    def unparsed(source: String): Command =
    2.58 @@ -333,7 +312,7 @@
    2.59      val id: Document_ID.Command,
    2.60      val node_name: Document.Node.Name,
    2.61      val blobs: List[Command.Blob],
    2.62 -    val span: List[Token],
    2.63 +    val span: Thy_Syntax.Span,
    2.64      val source: String,
    2.65      val init_results: Command.Results,
    2.66      val init_markup: Markup_Tree)
    2.67 @@ -341,14 +320,15 @@
    2.68    /* classification */
    2.69  
    2.70    def is_undefined: Boolean = id == Document_ID.none
    2.71 -  val is_unparsed: Boolean = span.exists(_.is_unparsed)
    2.72 -  val is_unfinished: Boolean = span.exists(_.is_unfinished)
    2.73 +  val is_unparsed: Boolean = span.content.exists(_.is_unparsed)
    2.74 +  val is_unfinished: Boolean = span.content.exists(_.is_unfinished)
    2.75  
    2.76 -  val is_ignored: Boolean = !span.exists(_.is_proper)
    2.77 -  val is_malformed: Boolean = !is_ignored && (!span.head.is_command || span.exists(_.is_error))
    2.78 -  def is_command: Boolean = !is_ignored && !is_malformed
    2.79 +  def is_command: Boolean = span.kind.isInstanceOf[Thy_Syntax.Command_Span]
    2.80 +  def is_ignored: Boolean = span.kind == Thy_Syntax.Ignored_Span
    2.81 +  def is_malformed: Boolean = span.kind == Thy_Syntax.Malformed_Span
    2.82  
    2.83 -  def name: String = Command.name(span)
    2.84 +  def name: String =
    2.85 +    span.kind match { case Thy_Syntax.Command_Span(name) => name case _ => "" }
    2.86  
    2.87    override def toString =
    2.88      id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
    2.89 @@ -379,7 +359,8 @@
    2.90    def range: Text.Range = chunk.range
    2.91  
    2.92    val proper_range: Text.Range =
    2.93 -    Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
    2.94 +    Text.Range(0,
    2.95 +      (length /: span.content.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
    2.96  
    2.97    def source(range: Text.Range): String = source.substring(range.start, range.stop)
    2.98  
     3.1 --- a/src/Pure/PIDE/prover.scala	Mon Aug 11 20:46:56 2014 +0200
     3.2 +++ b/src/Pure/PIDE/prover.scala	Mon Aug 11 22:29:48 2014 +0200
     3.3 @@ -15,7 +15,7 @@
     3.4    {
     3.5      def add_keywords(keywords: Thy_Header.Keywords): Syntax
     3.6      def scan(input: CharSequence): List[Token]
     3.7 -    def load(span: List[Token]): Option[List[String]]
     3.8 +    def load_command(name: String): Option[List[String]]
     3.9      def load_commands_in(text: String): Boolean
    3.10    }
    3.11  
     4.1 --- a/src/Pure/Thy/thy_syntax.ML	Mon Aug 11 20:46:56 2014 +0200
     4.2 +++ b/src/Pure/Thy/thy_syntax.ML	Mon Aug 11 22:29:48 2014 +0200
     4.3 @@ -9,7 +9,7 @@
     4.4    val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
     4.5    val reports_of_tokens: Token.T list -> bool * Position.report_text list
     4.6    val present_token: Token.T -> Output.output
     4.7 -  datatype span_kind = Command of string * Position.T | Ignored | Malformed
     4.8 +  datatype span_kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span
     4.9    datatype span = Span of span_kind * Token.T list
    4.10    val span_kind: span -> span_kind
    4.11    val span_content: span -> Token.T list
    4.12 @@ -69,9 +69,7 @@
    4.13  
    4.14  (** spans **)
    4.15  
    4.16 -(* type span *)
    4.17 -
    4.18 -datatype span_kind = Command of string * Position.T | Ignored | Malformed;
    4.19 +datatype span_kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span;
    4.20  datatype span = Span of span_kind * Token.T list;
    4.21  
    4.22  fun span_kind (Span (k, _)) = k;
    4.23 @@ -84,27 +82,29 @@
    4.24  
    4.25  local
    4.26  
    4.27 -fun make_span toks =
    4.28 -  if not (null toks) andalso Token.is_command (hd toks) then
    4.29 -    Span (Command (Token.content_of (hd toks), Token.pos_of (hd toks)), toks)
    4.30 -  else if forall Token.is_improper toks then Span (Ignored, toks)
    4.31 -  else Span (Malformed, toks);
    4.32 +fun ship span =
    4.33 +  let
    4.34 +    val kind =
    4.35 +      if not (null span) andalso Token.is_command (hd span) then
    4.36 +        Command_Span (Token.content_of (hd span), Token.pos_of (hd span))
    4.37 +      else if forall Token.is_improper span then Ignored_Span
    4.38 +      else Malformed_Span;
    4.39 +  in cons (Span (kind, span)) end;
    4.40  
    4.41 -fun flush (result, span, improper) =
    4.42 +fun flush (result, content, improper) =
    4.43    result
    4.44 -  |> not (null span) ? cons (rev span)
    4.45 -  |> not (null improper) ? cons (rev improper);
    4.46 +  |> not (null content) ? ship (rev content)
    4.47 +  |> not (null improper) ? ship (rev improper);
    4.48  
    4.49 -fun parse tok (result, span, improper) =
    4.50 -  if Token.is_command tok then (flush (result, span, improper), [tok], [])
    4.51 -  else if Token.is_improper tok then (result, span, tok :: improper)
    4.52 -  else (result, tok :: (improper @ span), []);
    4.53 +fun parse tok (result, content, improper) =
    4.54 +  if Token.is_command tok then (flush (result, content, improper), [tok], [])
    4.55 +  else if Token.is_improper tok then (result, content, tok :: improper)
    4.56 +  else (result, tok :: (improper @ content), []);
    4.57  
    4.58  in
    4.59  
    4.60  fun parse_spans toks =
    4.61 -  fold parse toks ([], [], [])
    4.62 -  |> flush |> rev |> map make_span;
    4.63 +  fold parse toks ([], [], []) |> flush |> rev;
    4.64  
    4.65  end;
    4.66  
    4.67 @@ -137,7 +137,7 @@
    4.68  
    4.69  fun resolve_files read_files span =
    4.70    (case span of
    4.71 -    Span (Command (cmd, pos), toks) =>
    4.72 +    Span (Command_Span (cmd, pos), toks) =>
    4.73        if Keyword.is_theory_load cmd then
    4.74          (case find_file (clean_tokens toks) of
    4.75            NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
    4.76 @@ -146,7 +146,7 @@
    4.77                val toks' = toks |> map_index (fn (j, tok) =>
    4.78                  if i = j then Token.put_files (read_files cmd path) tok
    4.79                  else tok);
    4.80 -            in Span (Command (cmd, pos), toks') end)
    4.81 +            in Span (Command_Span (cmd, pos), toks') end)
    4.82        else span
    4.83    | _ => span);
    4.84  
    4.85 @@ -174,9 +174,9 @@
    4.86  
    4.87  (* scanning spans *)
    4.88  
    4.89 -val eof = Span (Command ("", Position.none), []);
    4.90 +val eof = Span (Command_Span ("", Position.none), []);
    4.91  
    4.92 -fun is_eof (Span (Command ("", _), _)) = true
    4.93 +fun is_eof (Span (Command_Span ("", _), _)) = true
    4.94    | is_eof _ = false;
    4.95  
    4.96  val not_eof = not o is_eof;
    4.97 @@ -189,10 +189,10 @@
    4.98  local
    4.99  
   4.100  fun command_with pred =
   4.101 -  Scan.one (fn (Span (Command (name, _), _)) => pred name | _ => false);
   4.102 +  Scan.one (fn (Span (Command_Span (name, _), _)) => pred name | _ => false);
   4.103  
   4.104  val proof_atom =
   4.105 -  Scan.one (fn (Span (Command (name, _), _)) => Keyword.is_proof_body name | _ => true) >> atom;
   4.106 +  Scan.one (fn (Span (Command_Span (name, _), _)) => Keyword.is_proof_body name | _ => true) >> atom;
   4.107  
   4.108  fun proof_element x = (command_with Keyword.is_proof_goal -- proof_rest >> element || proof_atom) x
   4.109  and proof_rest x = (Scan.repeat proof_element -- command_with Keyword.is_qed) x;
     5.1 --- a/src/Pure/Thy/thy_syntax.scala	Mon Aug 11 20:46:56 2014 +0200
     5.2 +++ b/src/Pure/Thy/thy_syntax.scala	Mon Aug 11 22:29:48 2014 +0200
     5.3 @@ -13,23 +13,69 @@
     5.4  
     5.5  object Thy_Syntax
     5.6  {
     5.7 -  /** parse spans **/
     5.8 +  /** spans **/
     5.9  
    5.10 -  def parse_spans(toks: List[Token]): List[List[Token]] =
    5.11 +  sealed abstract class Span_Kind
    5.12 +  case class Command_Span(name: String) extends Span_Kind
    5.13 +  case object Ignored_Span extends Span_Kind
    5.14 +  case object Malformed_Span extends Span_Kind
    5.15 +
    5.16 +  sealed case class Span(kind: Span_Kind, content: List[Token])
    5.17    {
    5.18 -    val result = new mutable.ListBuffer[List[Token]]
    5.19 -    val span = new mutable.ListBuffer[Token]
    5.20 +    def compact_source: (String, Span) =
    5.21 +    {
    5.22 +      val source: String =
    5.23 +        content match {
    5.24 +          case List(tok) => tok.source
    5.25 +          case toks => toks.map(_.source).mkString
    5.26 +        }
    5.27 +
    5.28 +      val content1 = new mutable.ListBuffer[Token]
    5.29 +      var i = 0
    5.30 +      for (Token(kind, s) <- content) {
    5.31 +        val n = s.length
    5.32 +        val s1 = source.substring(i, i + n)
    5.33 +        content1 += Token(kind, s1)
    5.34 +        i += n
    5.35 +      }
    5.36 +      (source, Span(kind, content1.toList))
    5.37 +    }
    5.38 +  }
    5.39 +
    5.40 +  val empty_span: Span = Span(Ignored_Span, Nil)
    5.41 +
    5.42 +  def unparsed_span(source: String): Span =
    5.43 +    Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
    5.44 +
    5.45 +
    5.46 +  /* parse */
    5.47 +
    5.48 +  def parse_spans(toks: List[Token]): List[Span] =
    5.49 +  {
    5.50 +    val result = new mutable.ListBuffer[Span]
    5.51 +    val content = new mutable.ListBuffer[Token]
    5.52      val improper = new mutable.ListBuffer[Token]
    5.53  
    5.54 +    def ship(span: List[Token])
    5.55 +    {
    5.56 +      val kind =
    5.57 +        if (!span.isEmpty && span.head.is_command && !span.exists(_.is_error))
    5.58 +          Command_Span(span.head.source)
    5.59 +        else if (span.forall(_.is_improper)) Ignored_Span
    5.60 +        else Malformed_Span
    5.61 +      result += Span(kind, span)
    5.62 +    }
    5.63 +
    5.64      def flush()
    5.65      {
    5.66 -      if (!span.isEmpty) { result += span.toList; span.clear }
    5.67 -      if (!improper.isEmpty) { result += improper.toList; improper.clear }
    5.68 +      if (!content.isEmpty) { ship(content.toList); content.clear }
    5.69 +      if (!improper.isEmpty) { ship(improper.toList); improper.clear }
    5.70      }
    5.71 +
    5.72      for (tok <- toks) {
    5.73 -      if (tok.is_command) { flush(); span += tok }
    5.74 +      if (tok.is_command) { flush(); content += tok }
    5.75        else if (tok.is_improper) improper += tok
    5.76 -      else { span ++= improper; improper.clear; span += tok }
    5.77 +      else { content ++= improper; improper.clear; content += tok }
    5.78      }
    5.79      flush()
    5.80  
    5.81 @@ -185,23 +231,27 @@
    5.82      }
    5.83    }
    5.84  
    5.85 -  def span_files(syntax: Prover.Syntax, span: List[Token]): List[String] =
    5.86 -    syntax.load(span) match {
    5.87 -      case Some(exts) =>
    5.88 -        find_file(span) match {
    5.89 -          case Some(file) =>
    5.90 -            if (exts.isEmpty) List(file)
    5.91 -            else exts.map(ext => file + "." + ext)
    5.92 +  def span_files(syntax: Prover.Syntax, span: Span): List[String] =
    5.93 +    span.kind match {
    5.94 +      case Command_Span(name) =>
    5.95 +        syntax.load_command(name) match {
    5.96 +          case Some(exts) =>
    5.97 +            find_file(span.content) match {
    5.98 +              case Some(file) =>
    5.99 +                if (exts.isEmpty) List(file)
   5.100 +                else exts.map(ext => file + "." + ext)
   5.101 +              case None => Nil
   5.102 +            }
   5.103            case None => Nil
   5.104          }
   5.105 -      case None => Nil
   5.106 +      case _ => Nil
   5.107      }
   5.108  
   5.109    def resolve_files(
   5.110        resources: Resources,
   5.111        syntax: Prover.Syntax,
   5.112        node_name: Document.Node.Name,
   5.113 -      span: List[Token],
   5.114 +      span: Span,
   5.115        get_blob: Document.Node.Name => Option[Document.Blob])
   5.116      : List[Command.Blob] =
   5.117    {
   5.118 @@ -219,8 +269,8 @@
   5.119  
   5.120    @tailrec private def chop_common(
   5.121        cmds: List[Command],
   5.122 -      blobs_spans: List[(List[Command.Blob], List[Token])])
   5.123 -    : (List[Command], List[(List[Command.Blob], List[Token])]) =
   5.124 +      blobs_spans: List[(List[Command.Blob], Span)])
   5.125 +    : (List[Command], List[(List[Command.Blob], Span)]) =
   5.126    {
   5.127      (cmds, blobs_spans) match {
   5.128        case (cmd :: cmds, (blobs, span) :: rest) if cmd.blobs == blobs && cmd.span == span =>