# HG changeset patch
# User wenzelm
# Date 1365188095 -7200
# Node ID 589daaf48dba5c7f4d7595f39b4afa7989b05d1c
# Parent  e09446d3cacaca7ed22b966a1bd2a3976d7efdef
tuned signature -- agree with markup terminology;

diff -r e09446d3caca -r 589daaf48dba src/Pure/Isar/isar_syn.ML
--- 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);
 
 
 
diff -r e09446d3caca -r 589daaf48dba src/Pure/Isar/outer_syntax.ML
--- 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
diff -r e09446d3caca -r 589daaf48dba src/Pure/Isar/parse.ML
--- 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 *)
diff -r e09446d3caca -r 589daaf48dba src/Pure/Isar/parse.scala
--- 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] =
diff -r e09446d3caca -r 589daaf48dba src/Pure/Thy/thy_header.ML
--- 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;
 
diff -r e09446d3caca -r 589daaf48dba src/Pure/Thy/thy_header.scala
--- 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 }
   }
 
diff -r e09446d3caca -r 589daaf48dba src/Pure/Thy/thy_output.ML
--- 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 =>