more general notion of command span: command keyword not necessarily at start;
authorwenzelm
Sat Apr 04 21:21:40 2015 +0200 (2015-04-04)
changeset 59924801b979ec0c2
parent 59923 b21c82422d65
child 59925 32402fe5ae6a
more general notion of command span: command keyword not necessarily at start;
support for special 'private' prefix for local_theory commands;
clarified parse_spans, with related operations for document Thy_Output and editor Token_Markup;
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/outer_syntax.scala
src/Pure/Isar/parse.ML
src/Pure/Isar/token.ML
src/Pure/Isar/token.scala
src/Pure/PIDE/command.scala
src/Pure/Thy/thy_output.ML
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Sat Apr 04 14:04:11 2015 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sat Apr 04 21:21:40 2015 +0200
     1.3 @@ -42,16 +42,20 @@
     1.4  
     1.5  (* command parsers *)
     1.6  
     1.7 +datatype command_parser =
     1.8 +  Parser of (Toplevel.transition -> Toplevel.transition) parser |
     1.9 +  Private_Parser of Position.T option -> (Toplevel.transition -> Toplevel.transition) parser;
    1.10 +
    1.11  datatype command = Command of
    1.12   {comment: string,
    1.13 -  parse: (Toplevel.transition -> Toplevel.transition) parser,
    1.14 +  command_parser: command_parser,
    1.15    pos: Position.T,
    1.16    id: serial};
    1.17  
    1.18  fun eq_command (Command {id = id1, ...}, Command {id = id2, ...}) = id1 = id2;
    1.19  
    1.20 -fun new_command comment parse pos =
    1.21 -  Command {comment = comment, parse = parse, pos = pos, id = serial ()};
    1.22 +fun new_command comment command_parser pos =
    1.23 +  Command {comment = comment, command_parser = command_parser, pos = pos, id = serial ()};
    1.24  
    1.25  fun command_pos (Command {pos, ...}) = pos;
    1.26  
    1.27 @@ -132,16 +136,16 @@
    1.28  
    1.29  type command_spec = string * Position.T;
    1.30  
    1.31 -fun command (name, pos) comment parse =
    1.32 -  Theory.setup (add_command name (new_command comment parse pos));
    1.33 +fun raw_command (name, pos) comment command_parser =
    1.34 +  Theory.setup (add_command name (new_command comment command_parser pos));
    1.35  
    1.36 -val opt_private =
    1.37 -  Scan.option (Parse.$$$ "(" |-- (Parse.position (Parse.$$$ "private") >> #2) --| Parse.$$$ ")");
    1.38 +fun command (name, pos) comment parse =
    1.39 +  raw_command (name, pos) comment (Parser parse);
    1.40  
    1.41  fun local_theory_command trans command_spec comment parse =
    1.42 -  command command_spec comment
    1.43 -    (opt_private -- Parse.opt_target -- parse >>
    1.44 -      (fn ((private, target), f) => trans private target f));
    1.45 +  raw_command command_spec comment
    1.46 +    (Private_Parser (fn private =>
    1.47 +      Parse.opt_target -- parse >> (fn (target, f) => trans private target f)));
    1.48  
    1.49  val local_theory' = local_theory_command Toplevel.local_theory';
    1.50  val local_theory = local_theory_command Toplevel.local_theory;
    1.51 @@ -157,12 +161,17 @@
    1.52  local
    1.53  
    1.54  fun parse_command thy =
    1.55 -  Parse.position Parse.command_ :|-- (fn (name, pos) =>
    1.56 +  Scan.ahead (Parse.opt_private |-- Parse.position Parse.command_) :|-- (fn (name, pos) =>
    1.57      let
    1.58 +      val command_tags = Parse.command_ -- Parse.tags;
    1.59        val tr0 = Toplevel.empty |> Toplevel.name name |> Toplevel.position pos;
    1.60      in
    1.61        (case lookup_commands thy name of
    1.62 -        SOME (Command {parse, ...}) => Parse.!!! (Parse.tags |-- parse) >> (fn f => f tr0)
    1.63 +        SOME (Command {command_parser = Parser parse, ...}) =>
    1.64 +          Parse.!!! (command_tags |-- parse) >> (fn f => f tr0)
    1.65 +      | SOME (Command {command_parser = Private_Parser parse, ...}) =>
    1.66 +          Parse.opt_private :|-- (fn private =>
    1.67 +            Parse.!!! (command_tags |-- parse private)) >> (fn f => f tr0)
    1.68        | NONE =>
    1.69            Scan.succeed
    1.70              (tr0 |> Toplevel.imperative (fn () => err_command "Undefined command " name [pos])))
    1.71 @@ -200,10 +209,12 @@
    1.72  fun ship span =
    1.73    let
    1.74      val kind =
    1.75 -      if not (null span) andalso Token.is_command (hd span) andalso not (exists Token.is_error span)
    1.76 -      then Command_Span.Command_Span (Token.content_of (hd span), Token.pos_of (hd span))
    1.77 -      else if forall Token.is_improper span then Command_Span.Ignored_Span
    1.78 -      else Command_Span.Malformed_Span;
    1.79 +      if forall Token.is_improper span then Command_Span.Ignored_Span
    1.80 +      else if exists Token.is_error span then Command_Span.Malformed_Span
    1.81 +      else
    1.82 +        (case find_first Token.is_command span of
    1.83 +          NONE => Command_Span.Malformed_Span
    1.84 +        | SOME cmd => Command_Span.Command_Span (Token.content_of cmd, Token.pos_of cmd));
    1.85    in cons (Command_Span.Span (kind, span)) end;
    1.86  
    1.87  fun flush (result, content, improper) =
    1.88 @@ -212,8 +223,11 @@
    1.89    |> not (null improper) ? ship (rev improper);
    1.90  
    1.91  fun parse tok (result, content, improper) =
    1.92 -  if Token.is_command tok then (flush (result, content, improper), [tok], [])
    1.93 -  else if Token.is_improper tok then (result, content, tok :: improper)
    1.94 +  if Token.is_improper tok then (result, content, tok :: improper)
    1.95 +  else if Token.is_private tok orelse
    1.96 +    Token.is_command tok andalso
    1.97 +      (not (exists Token.is_private content) orelse exists Token.is_command content)
    1.98 +  then (flush (result, content, improper), [tok], [])
    1.99    else (result, tok :: (improper @ content), []);
   1.100  
   1.101  in
   1.102 @@ -246,4 +260,3 @@
   1.103    else [];
   1.104  
   1.105  end;
   1.106 -
     2.1 --- a/src/Pure/Isar/outer_syntax.scala	Sat Apr 04 14:04:11 2015 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sat Apr 04 21:21:40 2015 +0200
     2.3 @@ -149,7 +149,7 @@
     2.4  
     2.5    /* line-oriented structure */
     2.6  
     2.7 -  def line_structure(tokens: List[Token], struct: Outer_Syntax.Line_Structure)
     2.8 +  def line_structure(tokens: List[Token], structure: Outer_Syntax.Line_Structure)
     2.9      : Outer_Syntax.Line_Structure =
    2.10    {
    2.11      val improper1 = tokens.forall(_.is_improper)
    2.12 @@ -157,11 +157,11 @@
    2.13  
    2.14      val depth1 =
    2.15        if (tokens.exists(tok => tok.is_command_kind(keywords, Keyword.theory))) 0
    2.16 -      else if (command1) struct.after_span_depth
    2.17 -      else struct.span_depth
    2.18 +      else if (command1) structure.after_span_depth
    2.19 +      else structure.span_depth
    2.20  
    2.21      val (span_depth1, after_span_depth1) =
    2.22 -      ((struct.span_depth, struct.after_span_depth) /: tokens) {
    2.23 +      ((structure.span_depth, structure.after_span_depth) /: tokens) {
    2.24          case ((x, y), tok) =>
    2.25            if (tok.is_command) {
    2.26              if (tok.is_command_kind(keywords, Keyword.theory_goal))
    2.27 @@ -194,13 +194,20 @@
    2.28      def ship(span: List[Token])
    2.29      {
    2.30        val kind =
    2.31 -        if (span.nonEmpty && span.head.is_command && !span.exists(_.is_error)) {
    2.32 -          val name = span.head.source
    2.33 -          val pos = Position.Range(Text.Range(0, Symbol.iterator(name).length) + 1)
    2.34 -          Command_Span.Command_Span(name, pos)
    2.35 -        }
    2.36 -        else if (span.forall(_.is_improper)) Command_Span.Ignored_Span
    2.37 -        else Command_Span.Malformed_Span
    2.38 +        if (span.forall(_.is_improper)) Command_Span.Ignored_Span
    2.39 +        else if (span.exists(_.is_error)) Command_Span.Malformed_Span
    2.40 +        else
    2.41 +          span.find(_.is_command) match {
    2.42 +            case None => Command_Span.Malformed_Span
    2.43 +            case Some(cmd) =>
    2.44 +              val name = cmd.source
    2.45 +              val offset =
    2.46 +                (0 /: span.takeWhile(_ != cmd)) {
    2.47 +                  case (i, tok) => i + Symbol.iterator(tok.source).length }
    2.48 +              val end_offset = offset + Symbol.iterator(name).length
    2.49 +              val pos = Position.Range(Text.Range(offset, end_offset) + 1)
    2.50 +              Command_Span.Command_Span(name, pos)
    2.51 +          }
    2.52        result += Command_Span.Span(kind, span)
    2.53      }
    2.54  
    2.55 @@ -211,8 +218,10 @@
    2.56      }
    2.57  
    2.58      for (tok <- toks) {
    2.59 -      if (tok.is_command) { flush(); content += tok }
    2.60 -      else if (tok.is_improper) improper += tok
    2.61 +      if (tok.is_improper) improper += tok
    2.62 +      else if (tok.is_private ||
    2.63 +        tok.is_command && (!content.exists(_.is_private) || content.exists(_.is_command)))
    2.64 +      { flush(); content += tok }
    2.65        else { content ++= improper; improper.clear; content += tok }
    2.66      }
    2.67      flush()
     3.1 --- a/src/Pure/Isar/parse.ML	Sat Apr 04 14:04:11 2015 +0200
     3.2 +++ b/src/Pure/Isar/parse.ML	Sat Apr 04 21:21:40 2015 +0200
     3.3 @@ -103,6 +103,8 @@
     3.4    val literal_fact: string parser
     3.5    val propp: (string * string list) parser
     3.6    val termp: (string * string list) parser
     3.7 +  val private: Position.T parser
     3.8 +  val opt_private: Position.T option parser
     3.9    val target: (xstring * Position.T) parser
    3.10    val opt_target: (xstring * Position.T) option parser
    3.11    val args: Token.T list parser
    3.12 @@ -396,7 +398,10 @@
    3.13  val termp = term -- Scan.optional ($$$ "(" |-- !!! (is_terms --| $$$ ")")) [];
    3.14  
    3.15  
    3.16 -(* targets *)
    3.17 +(* target information *)
    3.18 +
    3.19 +val private = position ($$$ "private") >> #2;
    3.20 +val opt_private = Scan.option private;
    3.21  
    3.22  val target = ($$$ "(" -- $$$ "in") |-- !!! (position xname --| $$$ ")");
    3.23  val opt_target = Scan.option target;
     4.1 --- a/src/Pure/Isar/token.ML	Sat Apr 04 14:04:11 2015 +0200
     4.2 +++ b/src/Pure/Isar/token.ML	Sat Apr 04 21:21:40 2015 +0200
     4.3 @@ -43,10 +43,11 @@
     4.4    val stopper: T Scan.stopper
     4.5    val kind_of: T -> kind
     4.6    val is_kind: kind -> T -> bool
     4.7 -  val keyword_with: (string -> bool) -> T -> bool
     4.8 -  val ident_with: (string -> bool) -> T -> bool
     4.9    val is_command: T -> bool
    4.10    val is_name: T -> bool
    4.11 +  val keyword_with: (string -> bool) -> T -> bool
    4.12 +  val is_private: T -> bool
    4.13 +  val ident_with: (string -> bool) -> T -> bool
    4.14    val is_proper: T -> bool
    4.15    val is_improper: T -> bool
    4.16    val is_comment: T -> bool
    4.17 @@ -246,6 +247,8 @@
    4.18  fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
    4.19    | keyword_with _ _ = false;
    4.20  
    4.21 +val is_private = keyword_with (fn x => x = "private");
    4.22 +
    4.23  fun ident_with pred (Token (_, (Ident, x), _)) = pred x
    4.24    | ident_with _ _ = false;
    4.25  
     5.1 --- a/src/Pure/Isar/token.scala	Sat Apr 04 14:04:11 2015 +0200
     5.2 +++ b/src/Pure/Isar/token.scala	Sat Apr 04 21:21:40 2015 +0200
     5.3 @@ -259,6 +259,8 @@
     5.4    def is_begin: Boolean = is_keyword && source == "begin"
     5.5    def is_end: Boolean = is_command && source == "end"
     5.6  
     5.7 +  def is_private: Boolean = is_keyword && source == "private"
     5.8 +
     5.9    def is_begin_block: Boolean = is_command && source == "{"
    5.10    def is_end_block: Boolean = is_command && source == "}"
    5.11  
     6.1 --- a/src/Pure/PIDE/command.scala	Sat Apr 04 14:04:11 2015 +0200
     6.2 +++ b/src/Pure/PIDE/command.scala	Sat Apr 04 21:21:40 2015 +0200
     6.3 @@ -325,13 +325,11 @@
     6.4    }
     6.5  
     6.6    private def find_file(tokens: List[(Token, Int)]): Option[(String, Int)] =
     6.7 -    tokens match {
     6.8 -      case (tok, _) :: toks =>
     6.9 -        if (tok.is_command)
    6.10 -          toks.collectFirst({ case (t, i) if t.is_name => (t.content, i) })
    6.11 -        else None
    6.12 -      case Nil => None
    6.13 +    if (tokens.exists({ case (t, _) => t.is_command })) {
    6.14 +      tokens.dropWhile({ case (t, _) => !t.is_command }).
    6.15 +        collectFirst({ case (t, i) if t.is_name => (t.content, i) })
    6.16      }
    6.17 +    else None
    6.18  
    6.19    def span_files(syntax: Prover.Syntax, span: Command_Span.Span): (List[String], Int) =
    6.20      syntax.load_command(span.name) match {
     7.1 --- a/src/Pure/Thy/thy_output.ML	Sat Apr 04 14:04:11 2015 +0200
     7.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Apr 04 21:21:40 2015 +0200
     7.3 @@ -203,7 +203,7 @@
     7.4  
     7.5  (** present theory source **)
     7.6  
     7.7 -(*NB: arranging white space around command spans is a black art.*)
     7.8 +(*NB: arranging white space around command spans is a black art*)
     7.9  
    7.10  (* presentation tokens *)
    7.11  
    7.12 @@ -384,11 +384,12 @@
    7.13          in (SOME (name, pos', tags), (mk (name, source), (flag, d))) end));
    7.14  
    7.15      val command = Scan.peek (fn d =>
    7.16 -      Parse.position (Scan.one (Token.is_command)) --
    7.17 -      Scan.repeat tag
    7.18 -      >> (fn ((tok, pos), tags) =>
    7.19 -        let val name = Token.content_of tok
    7.20 -        in (SOME (name, pos, tags), (Basic_Token tok, (Latex.markup_false, d))) end));
    7.21 +      Scan.optional (Scan.one Token.is_private -- improper >> op ::) [] --
    7.22 +      Scan.one Token.is_command -- Scan.repeat tag
    7.23 +      >> (fn ((private, cmd), tags) =>
    7.24 +        map (fn tok => (NONE, (Basic_Token tok, ("", d)))) private @
    7.25 +          [(SOME (Token.content_of cmd, Token.pos_of cmd, tags),
    7.26 +            (Basic_Token cmd, (Latex.markup_false, d)))]));
    7.27  
    7.28      val cmt = Scan.peek (fn d =>
    7.29        Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.document_source) >>
    7.30 @@ -397,12 +398,13 @@
    7.31      val other = Scan.peek (fn d =>
    7.32         Parse.not_eof >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
    7.33  
    7.34 -    val token =
    7.35 -      ignored ||
    7.36 -      markup Keyword.is_document_heading Markup_Token Latex.markup_true ||
    7.37 -      markup Keyword.is_document_body Markup_Env_Token Latex.markup_true ||
    7.38 -      markup Keyword.is_document_raw (Verbatim_Token o #2) "" ||
    7.39 -      command || cmt || other;
    7.40 +    val tokens =
    7.41 +      (ignored ||
    7.42 +        markup Keyword.is_document_heading Markup_Token Latex.markup_true ||
    7.43 +        markup Keyword.is_document_body Markup_Env_Token Latex.markup_true ||
    7.44 +        markup Keyword.is_document_raw (Verbatim_Token o #2) "") >> single ||
    7.45 +      command ||
    7.46 +      (cmt || other) >> single;
    7.47  
    7.48  
    7.49      (* spans *)
    7.50 @@ -431,7 +433,7 @@
    7.51      val spans = toks
    7.52        |> take_suffix Token.is_space |> #1
    7.53        |> Source.of_list
    7.54 -      |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk token))
    7.55 +      |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk tokens >> flat))
    7.56        |> Source.source stopper (Scan.error (Scan.bulk span))
    7.57        |> Source.exhaust;
    7.58  
     8.1 --- a/src/Tools/jEdit/src/token_markup.scala	Sat Apr 04 14:04:11 2015 +0200
     8.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Sat Apr 04 21:21:40 2015 +0200
     8.3 @@ -207,7 +207,7 @@
     8.4    }
     8.5  
     8.6  
     8.7 -  /* line tokens */
     8.8 +  /* tokens from line (inclusive) */
     8.9  
    8.10    private def try_line_tokens(syntax: Outer_Syntax, buffer: JEditBuffer, line: Int)
    8.11      : Option[List[Token]] =
    8.12 @@ -250,23 +250,70 @@
    8.13      } yield Text.Info(Text.Range(i - tok.source.length, i), tok)
    8.14  
    8.15  
    8.16 +  /* tokens from offset (inclusive) */
    8.17 +
    8.18 +  def token_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset):
    8.19 +      Iterator[Text.Info[Token]] =
    8.20 +    if (JEdit_Lib.buffer_range(buffer).contains(offset))
    8.21 +      line_token_iterator(syntax, buffer, buffer.getLineOfOffset(offset), buffer.getLineCount).
    8.22 +        dropWhile(info => !info.range.contains(offset))
    8.23 +    else Iterator.empty
    8.24 +
    8.25 +  def token_reverse_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset):
    8.26 +      Iterator[Text.Info[Token]] =
    8.27 +    if (JEdit_Lib.buffer_range(buffer).contains(offset))
    8.28 +      line_token_reverse_iterator(syntax, buffer, buffer.getLineOfOffset(offset), -1).
    8.29 +        dropWhile(info => !info.range.contains(offset))
    8.30 +    else Iterator.empty
    8.31 +
    8.32 +
    8.33    /* command spans */
    8.34  
    8.35    def command_span(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset)
    8.36      : Option[Text.Info[Command_Span.Span]] =
    8.37    {
    8.38 +    def maybe_command_start(i: Text.Offset): Option[Text.Info[Token]] =
    8.39 +      token_reverse_iterator(syntax, buffer, i).
    8.40 +        find(info => info.info.is_private || info.info.is_command)
    8.41 +
    8.42 +    def maybe_command_stop(i: Text.Offset): Option[Text.Info[Token]] =
    8.43 +      token_iterator(syntax, buffer, i).
    8.44 +        find(info => info.info.is_private || info.info.is_command)
    8.45 +
    8.46      if (JEdit_Lib.buffer_range(buffer).contains(offset)) {
    8.47 -      val start =
    8.48 -        line_token_reverse_iterator(syntax, buffer, buffer.getLineOfOffset(offset), -1).
    8.49 -          dropWhile(info => !info.range.contains(offset)).
    8.50 -          collectFirst({ case Text.Info(range, tok) if tok.is_command => range.start }).
    8.51 -          getOrElse(0)
    8.52 +      val start_info =
    8.53 +      {
    8.54 +        val info1 = maybe_command_start(offset)
    8.55 +        info1 match {
    8.56 +          case Some(Text.Info(range1, tok1)) if tok1.is_command =>
    8.57 +            val info2 = maybe_command_start(range1.start - 1)
    8.58 +            info2 match {
    8.59 +              case Some(Text.Info(_, tok2)) if tok2.is_private => info2
    8.60 +              case _ => info1
    8.61 +            }
    8.62 +          case _ => info1
    8.63 +        }
    8.64 +      }
    8.65 +      val (start_is_private, start, start_next) =
    8.66 +        start_info match {
    8.67 +          case Some(Text.Info(range, tok)) => (tok.is_private, range.start, range.stop)
    8.68 +          case None => (false, 0, 0)
    8.69 +        }
    8.70 +
    8.71 +      val stop_info =
    8.72 +      {
    8.73 +        val info1 = maybe_command_stop(start_next)
    8.74 +        info1 match {
    8.75 +          case Some(Text.Info(range1, tok1)) if tok1.is_command && start_is_private =>
    8.76 +            maybe_command_stop(range1.stop)
    8.77 +          case _ => info1
    8.78 +        }
    8.79 +      }
    8.80        val stop =
    8.81 -        line_token_iterator(syntax, buffer, buffer.getLineOfOffset(start), buffer.getLineCount).
    8.82 -          dropWhile(info => !info.range.contains(start)).
    8.83 -          dropWhile(info => info.range.contains(start)).
    8.84 -          collectFirst({ case Text.Info(range, tok) if tok.is_command => range.start }).
    8.85 -          getOrElse(buffer.getLength)
    8.86 +        stop_info match {
    8.87 +          case Some(Text.Info(range, _)) => range.start
    8.88 +          case None => buffer.getLength
    8.89 +        }
    8.90  
    8.91        val text = JEdit_Lib.try_get_text(buffer, Text.Range(start, stop)).getOrElse("")
    8.92        val spans = syntax.parse_spans(text)