# HG changeset patch # User wenzelm # Date 1428175300 -7200 # Node ID 801b979ec0c2e14e91ff3dbcacf5cdeb2fc8d30c # Parent b21c82422d6501bc577f6a4f13fca892e1f76cb1 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; diff -r b21c82422d65 -r 801b979ec0c2 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Sat Apr 04 14:04:11 2015 +0200 +++ b/src/Pure/Isar/outer_syntax.ML Sat Apr 04 21:21:40 2015 +0200 @@ -42,16 +42,20 @@ (* command parsers *) +datatype command_parser = + Parser of (Toplevel.transition -> Toplevel.transition) parser | + Private_Parser of Position.T option -> (Toplevel.transition -> Toplevel.transition) parser; + datatype command = Command of {comment: string, - parse: (Toplevel.transition -> Toplevel.transition) parser, + command_parser: command_parser, pos: Position.T, id: serial}; fun eq_command (Command {id = id1, ...}, Command {id = id2, ...}) = id1 = id2; -fun new_command comment parse pos = - Command {comment = comment, parse = parse, pos = pos, id = serial ()}; +fun new_command comment command_parser pos = + Command {comment = comment, command_parser = command_parser, pos = pos, id = serial ()}; fun command_pos (Command {pos, ...}) = pos; @@ -132,16 +136,16 @@ type command_spec = string * Position.T; -fun command (name, pos) comment parse = - Theory.setup (add_command name (new_command comment parse pos)); +fun raw_command (name, pos) comment command_parser = + Theory.setup (add_command name (new_command comment command_parser pos)); -val opt_private = - Scan.option (Parse.$$$ "(" |-- (Parse.position (Parse.$$$ "private") >> #2) --| Parse.$$$ ")"); +fun command (name, pos) comment parse = + raw_command (name, pos) comment (Parser parse); fun local_theory_command trans command_spec comment parse = - command command_spec comment - (opt_private -- Parse.opt_target -- parse >> - (fn ((private, target), f) => trans private target f)); + raw_command command_spec comment + (Private_Parser (fn private => + Parse.opt_target -- parse >> (fn (target, f) => trans private target f))); val local_theory' = local_theory_command Toplevel.local_theory'; val local_theory = local_theory_command Toplevel.local_theory; @@ -157,12 +161,17 @@ local fun parse_command thy = - Parse.position Parse.command_ :|-- (fn (name, pos) => + Scan.ahead (Parse.opt_private |-- Parse.position Parse.command_) :|-- (fn (name, pos) => let + val command_tags = Parse.command_ -- Parse.tags; val tr0 = Toplevel.empty |> Toplevel.name name |> Toplevel.position pos; in (case lookup_commands thy name of - SOME (Command {parse, ...}) => Parse.!!! (Parse.tags |-- parse) >> (fn f => f tr0) + SOME (Command {command_parser = Parser parse, ...}) => + Parse.!!! (command_tags |-- parse) >> (fn f => f tr0) + | SOME (Command {command_parser = Private_Parser parse, ...}) => + Parse.opt_private :|-- (fn private => + Parse.!!! (command_tags |-- parse private)) >> (fn f => f tr0) | NONE => Scan.succeed (tr0 |> Toplevel.imperative (fn () => err_command "Undefined command " name [pos]))) @@ -200,10 +209,12 @@ fun ship span = let val kind = - if not (null span) andalso Token.is_command (hd span) andalso not (exists Token.is_error span) - then Command_Span.Command_Span (Token.content_of (hd span), Token.pos_of (hd span)) - else if forall Token.is_improper span then Command_Span.Ignored_Span - else Command_Span.Malformed_Span; + if forall Token.is_improper span then Command_Span.Ignored_Span + else if exists Token.is_error span then Command_Span.Malformed_Span + else + (case find_first Token.is_command span of + NONE => Command_Span.Malformed_Span + | SOME cmd => Command_Span.Command_Span (Token.content_of cmd, Token.pos_of cmd)); in cons (Command_Span.Span (kind, span)) end; fun flush (result, content, improper) = @@ -212,8 +223,11 @@ |> not (null improper) ? ship (rev improper); fun parse tok (result, content, improper) = - if Token.is_command tok then (flush (result, content, improper), [tok], []) - else if Token.is_improper tok then (result, content, tok :: improper) + if Token.is_improper tok then (result, content, tok :: improper) + else if Token.is_private tok orelse + Token.is_command tok andalso + (not (exists Token.is_private content) orelse exists Token.is_command content) + then (flush (result, content, improper), [tok], []) else (result, tok :: (improper @ content), []); in @@ -246,4 +260,3 @@ else []; end; - diff -r b21c82422d65 -r 801b979ec0c2 src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Sat Apr 04 14:04:11 2015 +0200 +++ b/src/Pure/Isar/outer_syntax.scala Sat Apr 04 21:21:40 2015 +0200 @@ -149,7 +149,7 @@ /* line-oriented structure */ - def line_structure(tokens: List[Token], struct: Outer_Syntax.Line_Structure) + def line_structure(tokens: List[Token], structure: Outer_Syntax.Line_Structure) : Outer_Syntax.Line_Structure = { val improper1 = tokens.forall(_.is_improper) @@ -157,11 +157,11 @@ val depth1 = if (tokens.exists(tok => tok.is_command_kind(keywords, Keyword.theory))) 0 - else if (command1) struct.after_span_depth - else struct.span_depth + else if (command1) structure.after_span_depth + else structure.span_depth val (span_depth1, after_span_depth1) = - ((struct.span_depth, struct.after_span_depth) /: tokens) { + ((structure.span_depth, structure.after_span_depth) /: tokens) { case ((x, y), tok) => if (tok.is_command) { if (tok.is_command_kind(keywords, Keyword.theory_goal)) @@ -194,13 +194,20 @@ def ship(span: List[Token]) { val kind = - if (span.nonEmpty && span.head.is_command && !span.exists(_.is_error)) { - val name = span.head.source - val pos = Position.Range(Text.Range(0, Symbol.iterator(name).length) + 1) - Command_Span.Command_Span(name, pos) - } - else if (span.forall(_.is_improper)) Command_Span.Ignored_Span - else Command_Span.Malformed_Span + if (span.forall(_.is_improper)) Command_Span.Ignored_Span + else if (span.exists(_.is_error)) Command_Span.Malformed_Span + else + span.find(_.is_command) match { + case None => Command_Span.Malformed_Span + case Some(cmd) => + val name = cmd.source + val offset = + (0 /: span.takeWhile(_ != cmd)) { + case (i, tok) => i + Symbol.iterator(tok.source).length } + val end_offset = offset + Symbol.iterator(name).length + val pos = Position.Range(Text.Range(offset, end_offset) + 1) + Command_Span.Command_Span(name, pos) + } result += Command_Span.Span(kind, span) } @@ -211,8 +218,10 @@ } for (tok <- toks) { - if (tok.is_command) { flush(); content += tok } - else if (tok.is_improper) improper += tok + if (tok.is_improper) improper += tok + else if (tok.is_private || + tok.is_command && (!content.exists(_.is_private) || content.exists(_.is_command))) + { flush(); content += tok } else { content ++= improper; improper.clear; content += tok } } flush() diff -r b21c82422d65 -r 801b979ec0c2 src/Pure/Isar/parse.ML --- a/src/Pure/Isar/parse.ML Sat Apr 04 14:04:11 2015 +0200 +++ b/src/Pure/Isar/parse.ML Sat Apr 04 21:21:40 2015 +0200 @@ -103,6 +103,8 @@ val literal_fact: string parser val propp: (string * string list) parser val termp: (string * string list) parser + val private: Position.T parser + val opt_private: Position.T option parser val target: (xstring * Position.T) parser val opt_target: (xstring * Position.T) option parser val args: Token.T list parser @@ -396,7 +398,10 @@ val termp = term -- Scan.optional ($$$ "(" |-- !!! (is_terms --| $$$ ")")) []; -(* targets *) +(* target information *) + +val private = position ($$$ "private") >> #2; +val opt_private = Scan.option private; val target = ($$$ "(" -- $$$ "in") |-- !!! (position xname --| $$$ ")"); val opt_target = Scan.option target; diff -r b21c82422d65 -r 801b979ec0c2 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Sat Apr 04 14:04:11 2015 +0200 +++ b/src/Pure/Isar/token.ML Sat Apr 04 21:21:40 2015 +0200 @@ -43,10 +43,11 @@ val stopper: T Scan.stopper val kind_of: T -> kind val is_kind: kind -> T -> bool - val keyword_with: (string -> bool) -> T -> bool - val ident_with: (string -> bool) -> T -> bool val is_command: T -> bool val is_name: T -> bool + val keyword_with: (string -> bool) -> T -> bool + val is_private: T -> bool + val ident_with: (string -> bool) -> T -> bool val is_proper: T -> bool val is_improper: T -> bool val is_comment: T -> bool @@ -246,6 +247,8 @@ fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x | keyword_with _ _ = false; +val is_private = keyword_with (fn x => x = "private"); + fun ident_with pred (Token (_, (Ident, x), _)) = pred x | ident_with _ _ = false; diff -r b21c82422d65 -r 801b979ec0c2 src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Sat Apr 04 14:04:11 2015 +0200 +++ b/src/Pure/Isar/token.scala Sat Apr 04 21:21:40 2015 +0200 @@ -259,6 +259,8 @@ def is_begin: Boolean = is_keyword && source == "begin" def is_end: Boolean = is_command && source == "end" + def is_private: Boolean = is_keyword && source == "private" + def is_begin_block: Boolean = is_command && source == "{" def is_end_block: Boolean = is_command && source == "}" diff -r b21c82422d65 -r 801b979ec0c2 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Sat Apr 04 14:04:11 2015 +0200 +++ b/src/Pure/PIDE/command.scala Sat Apr 04 21:21:40 2015 +0200 @@ -325,13 +325,11 @@ } 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 + if (tokens.exists({ case (t, _) => t.is_command })) { + tokens.dropWhile({ case (t, _) => !t.is_command }). + collectFirst({ case (t, i) if t.is_name => (t.content, i) }) } + else None def span_files(syntax: Prover.Syntax, span: Command_Span.Span): (List[String], Int) = syntax.load_command(span.name) match { diff -r b21c82422d65 -r 801b979ec0c2 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Sat Apr 04 14:04:11 2015 +0200 +++ b/src/Pure/Thy/thy_output.ML Sat Apr 04 21:21:40 2015 +0200 @@ -203,7 +203,7 @@ (** present theory source **) -(*NB: arranging white space around command spans is a black art.*) +(*NB: arranging white space around command spans is a black art*) (* presentation tokens *) @@ -384,11 +384,12 @@ in (SOME (name, pos', tags), (mk (name, source), (flag, d))) end)); val command = Scan.peek (fn d => - Parse.position (Scan.one (Token.is_command)) -- - Scan.repeat tag - >> (fn ((tok, pos), tags) => - let val name = Token.content_of tok - in (SOME (name, pos, tags), (Basic_Token tok, (Latex.markup_false, d))) end)); + Scan.optional (Scan.one Token.is_private -- improper >> op ::) [] -- + Scan.one Token.is_command -- Scan.repeat tag + >> (fn ((private, cmd), tags) => + map (fn tok => (NONE, (Basic_Token tok, ("", d)))) private @ + [(SOME (Token.content_of cmd, Token.pos_of cmd, tags), + (Basic_Token cmd, (Latex.markup_false, d)))])); val cmt = Scan.peek (fn d => Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.document_source) >> @@ -397,12 +398,13 @@ val other = Scan.peek (fn d => Parse.not_eof >> (fn tok => (NONE, (Basic_Token tok, ("", d))))); - val token = - ignored || - markup Keyword.is_document_heading Markup_Token Latex.markup_true || - markup Keyword.is_document_body Markup_Env_Token Latex.markup_true || - markup Keyword.is_document_raw (Verbatim_Token o #2) "" || - command || cmt || other; + val tokens = + (ignored || + markup Keyword.is_document_heading Markup_Token Latex.markup_true || + markup Keyword.is_document_body Markup_Env_Token Latex.markup_true || + markup Keyword.is_document_raw (Verbatim_Token o #2) "") >> single || + command || + (cmt || other) >> single; (* spans *) @@ -431,7 +433,7 @@ val spans = toks |> take_suffix Token.is_space |> #1 |> Source.of_list - |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk token)) + |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk tokens >> flat)) |> Source.source stopper (Scan.error (Scan.bulk span)) |> Source.exhaust; diff -r b21c82422d65 -r 801b979ec0c2 src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala Sat Apr 04 14:04:11 2015 +0200 +++ b/src/Tools/jEdit/src/token_markup.scala Sat Apr 04 21:21:40 2015 +0200 @@ -207,7 +207,7 @@ } - /* line tokens */ + /* tokens from line (inclusive) */ private def try_line_tokens(syntax: Outer_Syntax, buffer: JEditBuffer, line: Int) : Option[List[Token]] = @@ -250,23 +250,70 @@ } yield Text.Info(Text.Range(i - tok.source.length, i), tok) + /* tokens from offset (inclusive) */ + + def token_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset): + Iterator[Text.Info[Token]] = + if (JEdit_Lib.buffer_range(buffer).contains(offset)) + line_token_iterator(syntax, buffer, buffer.getLineOfOffset(offset), buffer.getLineCount). + dropWhile(info => !info.range.contains(offset)) + else Iterator.empty + + def token_reverse_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset): + Iterator[Text.Info[Token]] = + if (JEdit_Lib.buffer_range(buffer).contains(offset)) + line_token_reverse_iterator(syntax, buffer, buffer.getLineOfOffset(offset), -1). + dropWhile(info => !info.range.contains(offset)) + else Iterator.empty + + /* command spans */ def command_span(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset) : Option[Text.Info[Command_Span.Span]] = { + def maybe_command_start(i: Text.Offset): Option[Text.Info[Token]] = + token_reverse_iterator(syntax, buffer, i). + find(info => info.info.is_private || info.info.is_command) + + def maybe_command_stop(i: Text.Offset): Option[Text.Info[Token]] = + token_iterator(syntax, buffer, i). + find(info => info.info.is_private || info.info.is_command) + if (JEdit_Lib.buffer_range(buffer).contains(offset)) { - val start = - line_token_reverse_iterator(syntax, buffer, buffer.getLineOfOffset(offset), -1). - dropWhile(info => !info.range.contains(offset)). - collectFirst({ case Text.Info(range, tok) if tok.is_command => range.start }). - getOrElse(0) + val start_info = + { + val info1 = maybe_command_start(offset) + info1 match { + case Some(Text.Info(range1, tok1)) if tok1.is_command => + val info2 = maybe_command_start(range1.start - 1) + info2 match { + case Some(Text.Info(_, tok2)) if tok2.is_private => info2 + case _ => info1 + } + case _ => info1 + } + } + val (start_is_private, start, start_next) = + start_info match { + case Some(Text.Info(range, tok)) => (tok.is_private, range.start, range.stop) + case None => (false, 0, 0) + } + + val stop_info = + { + val info1 = maybe_command_stop(start_next) + info1 match { + case Some(Text.Info(range1, tok1)) if tok1.is_command && start_is_private => + maybe_command_stop(range1.stop) + case _ => info1 + } + } val stop = - line_token_iterator(syntax, buffer, buffer.getLineOfOffset(start), buffer.getLineCount). - dropWhile(info => !info.range.contains(start)). - dropWhile(info => info.range.contains(start)). - collectFirst({ case Text.Info(range, tok) if tok.is_command => range.start }). - getOrElse(buffer.getLength) + stop_info match { + case Some(Text.Info(range, _)) => range.start + case None => buffer.getLength + } val text = JEdit_Lib.try_get_text(buffer, Text.Range(start, stop)).getOrElse("") val spans = syntax.parse_spans(text)