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;

--- 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;
-

--- 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()

--- 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;

--- 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;
 

--- 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 == "}"
 

--- 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 {

--- 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;
 

--- 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)