--- a/src/Pure/Isar/isar_syn.ML Fri Apr 05 20:43:43 2013 +0200
+++ b/src/Pure/Isar/isar_syn.ML Fri Apr 05 20:54:55 2013 +0200
@@ -12,62 +12,62 @@
val _ =
Outer_Syntax.markup_command Thy_Output.Markup
@{command_spec "header"} "theory header"
- (Parse.doc_source >> Isar_Cmd.header_markup);
+ (Parse.document_source >> Isar_Cmd.header_markup);
val _ =
Outer_Syntax.markup_command Thy_Output.Markup
@{command_spec "chapter"} "chapter heading"
- (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
+ (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup);
val _ =
Outer_Syntax.markup_command Thy_Output.Markup
@{command_spec "section"} "section heading"
- (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
+ (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup);
val _ =
Outer_Syntax.markup_command Thy_Output.Markup
@{command_spec "subsection"} "subsection heading"
- (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
+ (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup);
val _ =
Outer_Syntax.markup_command Thy_Output.Markup
@{command_spec "subsubsection"} "subsubsection heading"
- (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
+ (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup);
val _ =
Outer_Syntax.markup_command Thy_Output.MarkupEnv
@{command_spec "text"} "formal comment (theory)"
- (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
+ (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup);
val _ =
Outer_Syntax.markup_command Thy_Output.Verbatim
@{command_spec "text_raw"} "raw document preparation text"
- (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
+ (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup);
val _ =
Outer_Syntax.markup_command Thy_Output.Markup
@{command_spec "sect"} "formal comment (proof)"
- (Parse.doc_source >> Isar_Cmd.proof_markup);
+ (Parse.document_source >> Isar_Cmd.proof_markup);
val _ =
Outer_Syntax.markup_command Thy_Output.Markup
@{command_spec "subsect"} "formal comment (proof)"
- (Parse.doc_source >> Isar_Cmd.proof_markup);
+ (Parse.document_source >> Isar_Cmd.proof_markup);
val _ =
Outer_Syntax.markup_command Thy_Output.Markup
@{command_spec "subsubsect"} "formal comment (proof)"
- (Parse.doc_source >> Isar_Cmd.proof_markup);
+ (Parse.document_source >> Isar_Cmd.proof_markup);
val _ =
Outer_Syntax.markup_command Thy_Output.MarkupEnv
@{command_spec "txt"} "formal comment (proof)"
- (Parse.doc_source >> Isar_Cmd.proof_markup);
+ (Parse.document_source >> Isar_Cmd.proof_markup);
val _ =
Outer_Syntax.markup_command Thy_Output.Verbatim
@{command_spec "txt_raw"} "raw document preparation text (proof)"
- (Parse.doc_source >> Isar_Cmd.proof_markup);
+ (Parse.document_source >> Isar_Cmd.proof_markup);
--- a/src/Pure/Isar/outer_syntax.ML Fri Apr 05 20:43:43 2013 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Fri Apr 05 20:54:55 2013 +0200
@@ -235,7 +235,7 @@
src
|> Token.source_proper
|> Source.source Token.stopper
- (Scan.bulk (Parse.$$$ "--" -- Parse.!!! Parse.doc_source >> K NONE || Parse.not_eof >> SOME))
+ (Scan.bulk (Parse.$$$ "--" -- Parse.!!! Parse.document_source >> K NONE || Parse.not_eof >> SOME))
(Option.map recover do_recover)
|> Source.map_filter I
|> Source.source Token.stopper
--- a/src/Pure/Isar/parse.ML Fri Apr 05 20:43:43 2013 +0200
+++ b/src/Pure/Isar/parse.ML Fri Apr 05 20:54:55 2013 +0200
@@ -91,7 +91,7 @@
val fixes: (binding * string option * mixfix) list parser
val for_fixes: (binding * string option * mixfix) list parser
val ML_source: (Symbol_Pos.text * Position.T) parser
- val doc_source: (Symbol_Pos.text * Position.T) parser
+ val document_source: (Symbol_Pos.text * Position.T) parser
val term_group: string parser
val prop_group: string parser
val term: string parser
@@ -341,7 +341,7 @@
(* embedded source text *)
val ML_source = source_position (group (fn () => "ML source") text);
-val doc_source = source_position (group (fn () => "document source") text);
+val document_source = source_position (group (fn () => "document source") text);
(* terms *)
--- a/src/Pure/Isar/parse.scala Fri Apr 05 20:43:43 2013 +0200
+++ b/src/Pure/Isar/parse.scala Fri Apr 05 20:54:55 2013 +0200
@@ -59,7 +59,7 @@
def xname: Parser[String] = atom("name reference", _.is_xname)
def text: Parser[String] = atom("text", _.is_text)
def ML_source: Parser[String] = atom("ML source", _.is_text)
- def doc_source: Parser[String] = atom("document source", _.is_text)
+ def document_source: Parser[String] = atom("document source", _.is_text)
def path: Parser[String] =
atom("file name/path specification", tok => tok.is_name && Path.is_ok(tok.content))
def theory_name: Parser[String] =
--- a/src/Pure/Thy/thy_header.ML Fri Apr 05 20:43:43 2013 +0200
+++ b/src/Pure/Thy/thy_header.ML Fri Apr 05 20:54:55 2013 +0200
@@ -118,7 +118,7 @@
val header =
(Parse.command_name headerN -- Parse.tags) |--
- (Parse.!!! (Parse.doc_source -- Scan.repeat Parse.semicolon --
+ (Parse.!!! (Parse.document_source -- Scan.repeat Parse.semicolon --
(Parse.command_name theoryN -- Parse.tags) |-- args)) ||
(Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args;
--- a/src/Pure/Thy/thy_header.scala Fri Apr 05 20:43:43 2013 +0200
+++ b/src/Pure/Thy/thy_header.scala Fri Apr 05 20:54:55 2013 +0200
@@ -73,7 +73,7 @@
{ case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
(keyword(HEADER) ~ tags) ~!
- ((doc_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
+ ((document_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
(keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
}
--- a/src/Pure/Thy/thy_output.ML Fri Apr 05 20:43:43 2013 +0200
+++ b/src/Pure/Thy/thy_output.ML Fri Apr 05 20:54:55 2013 +0200
@@ -379,7 +379,7 @@
improper |--
Parse.position (Scan.one (Token.is_command andf is_markup mark o Token.content_of)) --
Scan.repeat tag --
- Parse.!!!! ((improper -- locale -- improper) |-- Parse.doc_source --| improper_end)
+ Parse.!!!! ((improper -- locale -- improper) |-- Parse.document_source --| improper_end)
>> (fn (((tok, pos), tags), txt) =>
let val name = Token.content_of tok
in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end));
@@ -392,7 +392,7 @@
in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
val cmt = Scan.peek (fn d =>
- Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.doc_source)
+ Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.document_source)
>> (fn txt => (NONE, (MarkupToken ("cmt", txt), ("", d)))));
val other = Scan.peek (fn d =>