# HG changeset patch
# User wenzelm
# Date 1427279992 -3600
# Node ID 87641097d0f369ebd97cb9664a0faac52f860731
# Parent  3b6ad54b04fc2c1a8388767da892447a9a85f9bd
tuned signature;

diff -r 3b6ad54b04fc -r 87641097d0f3 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Wed Mar 25 10:59:28 2015 +0100
+++ b/src/Doc/antiquote_setup.ML	Wed Mar 25 11:39:52 2015 +0100
@@ -74,7 +74,7 @@
   (Input.source_content source, ML_Lex.read_source false source);
 
 fun index_ml name kind ml = Thy_Output.antiquotation name
-  (Scan.lift (Args.text_source_position -- Scan.option (Args.colon |-- Args.text_source_position)))
+  (Scan.lift (Args.text_input -- Scan.option (Args.colon |-- Args.text_input)))
   (fn {context = ctxt, ...} => fn (source1, opt_source2) =>
     let
       val (txt1, toks1) = prep_ml source1;
diff -r 3b6ad54b04fc -r 87641097d0f3 src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Wed Mar 25 10:59:28 2015 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Wed Mar 25 11:39:52 2015 +0100
@@ -144,7 +144,7 @@
 setup -- "document antiquotation"
 \<open>
   Thy_Output.antiquotation @{binding ML_cartouche}
-    (Scan.lift Args.cartouche_source_position) (fn {context, ...} => fn source =>
+    (Scan.lift Args.cartouche_input) (fn {context, ...} => fn source =>
       let
         val toks = ML_Lex.read "fn _ => (" @ ML_Lex.read_source false source @ ML_Lex.read ");";
         val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags (Input.pos_of source) toks;
@@ -179,7 +179,7 @@
 ML \<open>
   Outer_Syntax.command
     @{command_spec "text_cartouche"} ""
-    (Parse.opt_target -- Parse.source_position Parse.cartouche >> Thy_Output.document_command)
+    (Parse.opt_target -- Parse.input Parse.cartouche >> Thy_Output.document_command)
 \<close>
 
 text_cartouche
@@ -225,7 +225,7 @@
 subsubsection \<open>Explicit version: method with cartouche argument\<close>
 
 method_setup ml_tactic = \<open>
-  Scan.lift Args.cartouche_source_position
+  Scan.lift Args.cartouche_input
     >> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt))
 \<close>
 
@@ -246,7 +246,7 @@
 subsubsection \<open>Implicit version: method with special name "cartouche" (dynamic!)\<close>
 
 method_setup "cartouche" = \<open>
-  Scan.lift Args.cartouche_source_position
+  Scan.lift Args.cartouche_input
     >> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt))
 \<close>
 
diff -r 3b6ad54b04fc -r 87641097d0f3 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Wed Mar 25 10:59:28 2015 +0100
+++ b/src/Pure/Isar/args.ML	Wed Mar 25 11:39:52 2015 +0100
@@ -22,11 +22,11 @@
   val mode: string -> bool parser
   val maybe: 'a parser -> 'a option parser
   val cartouche_inner_syntax: string parser
-  val cartouche_source_position: Input.source parser
-  val text_source_position: Input.source parser
+  val cartouche_input: Input.source parser
+  val text_input: Input.source parser
   val text: string parser
   val name_inner_syntax: string parser
-  val name_source_position: Input.source parser
+  val name_input: Input.source parser
   val name: string parser
   val binding: binding parser
   val alt_name: string parser
@@ -108,14 +108,14 @@
 
 val cartouche = Parse.token Parse.cartouche;
 val cartouche_inner_syntax = cartouche >> Token.inner_syntax_of;
-val cartouche_source_position = cartouche >> Token.source_position_of;
+val cartouche_input = cartouche >> Token.input_of;
 
 val text_token = named || Parse.token (Parse.verbatim || Parse.cartouche);
-val text_source_position = text_token >> Token.source_position_of;
+val text_input = text_token >> Token.input_of;
 val text = text_token >> Token.content_of;
 
 val name_inner_syntax = named >> Token.inner_syntax_of;
-val name_source_position = named >> Token.source_position_of;
+val name_input = named >> Token.input_of;
 
 val name = named >> Token.content_of;
 val binding = Parse.position name >> Binding.make;
@@ -158,12 +158,10 @@
   named >> evaluate Token.Attribute (fn tok => att (Token.content_of tok, Token.pos_of tok));
 
 fun text_declaration read =
-  internal_declaration ||
-  text_token >> evaluate Token.Declaration (read o Token.source_position_of);
+  internal_declaration || text_token >> evaluate Token.Declaration (read o Token.input_of);
 
 fun cartouche_declaration read =
-  internal_declaration ||
-  cartouche >> evaluate Token.Declaration (read o Token.source_position_of);
+  internal_declaration || cartouche >> evaluate Token.Declaration (read o Token.input_of);
 
 
 (* terms and types *)
diff -r 3b6ad54b04fc -r 87641097d0f3 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Wed Mar 25 10:59:28 2015 +0100
+++ b/src/Pure/Isar/parse.ML	Wed Mar 25 11:39:52 2015 +0100
@@ -16,7 +16,7 @@
   val token: 'a parser -> Token.T parser
   val range: 'a parser -> ('a * Position.range) parser
   val position: 'a parser -> ('a * Position.T) parser
-  val source_position: 'a parser -> Input.source parser
+  val input: 'a parser -> Input.source parser
   val inner_syntax: 'a parser -> string parser
   val command_: string parser
   val keyword: string parser
@@ -176,7 +176,7 @@
 
 fun range scan = (Scan.ahead not_eof >> (Token.range_of o single)) -- scan >> Library.swap;
 fun position scan = (Scan.ahead not_eof >> Token.pos_of) -- scan >> Library.swap;
-fun source_position atom = Scan.ahead atom |-- not_eof >> Token.source_position_of;
+fun input atom = Scan.ahead atom |-- not_eof >> Token.input_of;
 fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.inner_syntax_of;
 
 fun kind k =
@@ -368,8 +368,8 @@
 
 (* embedded source text *)
 
-val ML_source = source_position (group (fn () => "ML source") text);
-val document_source = source_position (group (fn () => "document source") text);
+val ML_source = input (group (fn () => "ML source") text);
+val document_source = input (group (fn () => "document source") text);
 
 
 (* terms *)
diff -r 3b6ad54b04fc -r 87641097d0f3 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Wed Mar 25 10:59:28 2015 +0100
+++ b/src/Pure/Isar/token.ML	Wed Mar 25 11:39:52 2015 +0100
@@ -56,7 +56,7 @@
   val is_blank: T -> bool
   val is_newline: T -> bool
   val content_of: T -> string
-  val source_position_of: T -> Input.source
+  val input_of: T -> Input.source
   val inner_syntax_of: T -> string
   val keyword_markup: bool * Markup.T -> string -> Markup.T
   val completion_report: T -> Position.report_text list
@@ -281,12 +281,12 @@
 
 fun content_of (Token (_, (_, x), _)) = x;
 
-fun source_position_of (Token ((source, range), (kind, _), _)) =
+fun input_of (Token ((source, range), (kind, _), _)) =
   Input.source (delimited_kind kind) source range;
 
 fun inner_syntax_of tok =
   let val x = content_of tok
-  in if YXML.detect x then x else Syntax.implode_input (source_position_of tok) end;
+  in if YXML.detect x then x else Syntax.implode_input (input_of tok) end;
 
 
 (* markup reports *)
diff -r 3b6ad54b04fc -r 87641097d0f3 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Wed Mar 25 10:59:28 2015 +0100
+++ b/src/Pure/PIDE/command.ML	Wed Mar 25 11:39:52 2015 +0100
@@ -181,7 +181,7 @@
   Toplevel.setmp_thread_position tr
     (fn () =>
       Outer_Syntax.side_comments span |> maps (fn cmt =>
-        (Thy_Output.check_text (Token.source_position_of cmt) st'; [])
+        (Thy_Output.check_text (Token.input_of cmt) st'; [])
           handle exn =>
             if Exn.is_interrupt exn then reraise exn
             else Runtime.exn_messages_ids exn)) ();
diff -r 3b6ad54b04fc -r 87641097d0f3 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Wed Mar 25 10:59:28 2015 +0100
+++ b/src/Pure/Thy/latex.ML	Wed Mar 25 11:39:52 2015 +0100
@@ -132,7 +132,7 @@
       enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
     else if Token.is_kind Token.Verbatim tok then
       let
-        val ants = Antiquote.read (Token.source_position_of tok);
+        val ants = Antiquote.read (Token.input_of tok);
         val out = implode (map output_syms_antiq ants);
       in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
     else if Token.is_kind Token.Cartouche tok then
diff -r 3b6ad54b04fc -r 87641097d0f3 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Wed Mar 25 10:59:28 2015 +0100
+++ b/src/Pure/Thy/thy_output.ML	Wed Mar 25 11:39:52 2015 +0100
@@ -600,7 +600,7 @@
   basic_entity @{binding typ} Args.typ_abbrev Syntax.pretty_typ #>
   basic_entity @{binding class} (Scan.lift Args.name_inner_syntax) pretty_class #>
   basic_entity @{binding type} (Scan.lift Args.name) pretty_type #>
-  basic_entity @{binding text} (Scan.lift Args.text_source_position) pretty_text_report #>
+  basic_entity @{binding text} (Scan.lift Args.text_input) pretty_text_report #>
   basic_entities @{binding prf} Attrib.thms (pretty_prf false) #>
   basic_entities @{binding full_prf} Attrib.thms (pretty_prf true) #>
   basic_entity @{binding theory} (Scan.lift (Parse.position Args.name)) pretty_theory);
@@ -672,7 +672,7 @@
 
 local
 
-fun ml_text name ml = antiquotation name (Scan.lift Args.text_source_position)
+fun ml_text name ml = antiquotation name (Scan.lift Args.text_input)
   (fn {context = ctxt, ...} => fn source =>
    (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source) (ml source);
     verbatim_text ctxt (Input.source_content source)));
diff -r 3b6ad54b04fc -r 87641097d0f3 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Wed Mar 25 10:59:28 2015 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Wed Mar 25 11:39:52 2015 +0100
@@ -27,7 +27,7 @@
 fun reports_of_token keywords tok =
   let
     val malformed_symbols =
-      Input.source_explode (Token.source_position_of tok)
+      Input.source_explode (Token.input_of tok)
       |> map_filter (fn (sym, pos) =>
           if Symbol.is_malformed sym
           then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
diff -r 3b6ad54b04fc -r 87641097d0f3 src/Pure/Tools/rail.ML
--- a/src/Pure/Tools/rail.ML	Wed Mar 25 10:59:28 2015 +0100
+++ b/src/Pure/Tools/rail.ML	Wed Mar 25 11:39:52 2015 +0100
@@ -364,7 +364,7 @@
 
 val _ = Theory.setup
   (Thy_Output.antiquotation @{binding rail}
-    (Scan.lift (Parse.source_position (Parse.string || Parse.cartouche)))
+    (Scan.lift (Parse.input (Parse.string || Parse.cartouche)))
     (fn {state, context, ...} => output_rules state o read context));
 
 end;