# HG changeset patch
# User wenzelm
# Date 1427194398 -3600
# Node ID d453c69596cc0d546f76c813de63621e8f4830d3
# Parent  f19f4afa49e289f07dd98354af7983be46b5c94d
clarified input source;

diff -r f19f4afa49e2 -r d453c69596cc src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Mar 23 23:16:40 2015 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Mar 24 11:53:18 2015 +0100
@@ -412,7 +412,7 @@
 
 fun read_class ctxt text =
   let
-    val source = Syntax.read_token text;
+    val source = Syntax.read_input text;
     val (c, reports) = check_class ctxt (Input.source_content source, Input.pos_of source);
     val _ = Position.reports reports;
   in c end;
@@ -480,7 +480,7 @@
 
 fun read_type_name ctxt flags text =
   let
-    val source = Syntax.read_token text;
+    val source = Syntax.read_input text;
     val (T, reports) =
       check_type_name ctxt flags (Input.source_content source, Input.pos_of source);
     val _ = Position.reports reports;
@@ -530,7 +530,7 @@
 
 fun read_const ctxt flags text =
   let
-    val source = Syntax.read_token text;
+    val source = Syntax.read_input text;
     val (t, reports) = check_const ctxt flags (Input.source_content source, [Input.pos_of source]);
     val _ = Position.reports reports;
   in t end;
@@ -945,7 +945,7 @@
 fun retrieve pick context (Facts.Fact s) =
       let
         val ctxt = Context.the_proof context;
-        val pos = Syntax.read_token_pos s;
+        val pos = Syntax.read_input_pos s;
         val prop =
           Syntax.read_prop (ctxt |> set_mode mode_default |> allow_dummies) s
           |> singleton (Variable.polymorphic ctxt);
diff -r f19f4afa49e2 -r d453c69596cc src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Mon Mar 23 23:16:40 2015 +0100
+++ b/src/Pure/Isar/token.ML	Tue Mar 24 11:53:18 2015 +0100
@@ -55,9 +55,9 @@
   val is_space: T -> bool
   val is_blank: T -> bool
   val is_newline: T -> bool
-  val inner_syntax_of: T -> string
+  val content_of: T -> string
   val source_position_of: T -> Input.source
-  val content_of: T -> string
+  val inner_syntax_of: T -> string
   val keyword_markup: bool * Markup.T -> string -> Markup.T
   val completion_report: T -> Position.report_text list
   val reports: Keyword.keywords -> T -> Position.report_text list
@@ -279,18 +279,14 @@
 
 (* token content *)
 
-fun inner_syntax_of (Token ((source, (pos, _)), (kind, x), _)) =
-  if YXML.detect x then x
-  else
-    let
-      val delimited = delimited_kind kind;
-      val tree = XML.Elem (Markup.token delimited (Position.properties_of pos), [XML.Text source]);
-    in YXML.string_of tree end;
+fun content_of (Token (_, (_, x), _)) = x;
 
 fun source_position_of (Token ((source, range), (kind, _), _)) =
   Input.source (delimited_kind kind) source range;
 
-fun content_of (Token (_, (_, x), _)) = x;
+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;
 
 
 (* markup reports *)
diff -r f19f4afa49e2 -r d453c69596cc src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Mon Mar 23 23:16:40 2015 +0100
+++ b/src/Pure/PIDE/markup.ML	Tue Mar 24 11:53:18 2015 +0100
@@ -114,13 +114,13 @@
   val document_antiquotation_optionN: string
   val paragraphN: string val paragraph: T
   val text_foldN: string val text_fold: T
+  val inputN: string val input: bool -> Properties.T -> T
   val commandN: string val command: T
   val stringN: string val string: T
   val alt_stringN: string val alt_string: T
   val verbatimN: string val verbatim: T
   val cartoucheN: string val cartouche: T
   val commentN: string val comment: T
-  val tokenN: string val token: bool -> Properties.T -> T
   val keyword1N: string val keyword1: T
   val keyword2N: string val keyword2: T
   val keyword3N: string val keyword3: T
@@ -456,6 +456,12 @@
 val (text_foldN, text_fold) = markup_elem "text_fold";
 
 
+(* formal input *)
+
+val inputN = "input";
+fun input delimited props = (inputN, (delimitedN, print_bool delimited) :: props);
+
+
 (* outer syntax *)
 
 val (commandN, command) = markup_elem "command";
@@ -471,9 +477,6 @@
 val (cartoucheN, cartouche) = markup_elem "cartouche";
 val (commentN, comment) = markup_elem "comment";
 
-val tokenN = "token";
-fun token delimited props = (tokenN, (delimitedN, print_bool delimited) :: props);
-
 
 (* timing *)
 
diff -r f19f4afa49e2 -r d453c69596cc src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon Mar 23 23:16:40 2015 +0100
+++ b/src/Pure/Syntax/syntax.ML	Tue Mar 24 11:53:18 2015 +0100
@@ -14,9 +14,11 @@
   val ambiguity_warning: bool Config.T
   val ambiguity_limit_raw: Config.raw
   val ambiguity_limit: int Config.T
-  val read_token_pos: string -> Position.T
-  val read_token: string -> Input.source
-  val parse_token: Proof.context -> (XML.tree list -> 'a) ->
+  val encode_input: Input.source -> XML.tree
+  val implode_input: Input.source -> string
+  val read_input_pos: string -> Position.T
+  val read_input: string -> Input.source
+  val parse_input: Proof.context -> (XML.tree list -> 'a) ->
     (bool -> Markup.T) -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a
   val parse_sort: Proof.context -> string -> sort
   val parse_typ: Proof.context -> string -> typ
@@ -159,33 +161,42 @@
 val ambiguity_limit = Config.int ambiguity_limit_raw;
 
 
-(* outer syntax token -- with optional YXML content *)
+(* formal input *)
+
+fun encode_input source =
+  let
+    val delimited = Input.is_delimited source;
+    val pos = Input.pos_of source;
+    val text = Input.text_of source;
+  in XML.Elem (Markup.input delimited (Position.properties_of pos), [XML.Text text]) end;
+
+val implode_input = encode_input #> YXML.string_of;
 
 local
 
-fun token_range (XML.Elem ((name, props), _)) =
-      if name = Markup.tokenN
+fun input_range (XML.Elem ((name, props), _)) =
+      if name = Markup.inputN
       then (Markup.is_delimited props, Position.range_of_properties props)
       else (false, Position.no_range)
-  | token_range (XML.Text _) = (false, Position.no_range);
+  | input_range (XML.Text _) = (false, Position.no_range);
 
-fun token_source tree : Input.source =
+fun input_source tree =
   let
     val text = XML.content_of [tree];
-    val (delimited, range) = token_range tree;
+    val (delimited, range) = input_range tree;
   in Input.source delimited text range end;
 
 in
 
-fun read_token_pos str = #1 (#2 (token_range (YXML.parse str handle Fail msg => error msg)));
+fun read_input_pos str = #1 (#2 (input_range (YXML.parse str handle Fail msg => error msg)));
 
-fun read_token str = token_source (YXML.parse str handle Fail msg => error msg);
+fun read_input str = input_source (YXML.parse str handle Fail msg => error msg);
 
-fun parse_token ctxt decode markup parse str =
+fun parse_input ctxt decode markup parse str =
   let
     fun parse_tree tree =
       let
-        val source = token_source tree;
+        val source = input_source tree;
         val syms = Input.source_explode source;
         val pos = Input.pos_of source;
         val _ = Context_Position.report ctxt pos (markup (Input.is_delimited source));
@@ -193,7 +204,7 @@
   in
     (case YXML.parse_body str handle Fail msg => error msg of
       body as [tree as XML.Elem ((name, _), _)] =>
-        if name = Markup.tokenN then parse_tree tree else decode body
+        if name = Markup.inputN then parse_tree tree else decode body
     | [tree as XML.Text _] => parse_tree tree
     | body => decode body)
   end;
diff -r f19f4afa49e2 -r d453c69596cc src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Mon Mar 23 23:16:40 2015 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Mar 24 11:53:18 2015 +0100
@@ -365,7 +365,7 @@
     Markup.markup_report (Context_Position.reported_text ctxt pos Markup.bad ""));
 
 fun parse_sort ctxt =
-  Syntax.parse_token ctxt Term_XML.Decode.sort Markup.language_sort
+  Syntax.parse_input ctxt Term_XML.Decode.sort Markup.language_sort
     (fn (syms, pos) =>
       parse_tree ctxt "sort" (syms, pos)
       |> uncurry (report_result ctxt pos)
@@ -374,7 +374,7 @@
       handle ERROR msg => parse_failed ctxt pos msg "sort");
 
 fun parse_typ ctxt =
-  Syntax.parse_token ctxt Term_XML.Decode.typ Markup.language_type
+  Syntax.parse_input ctxt Term_XML.Decode.typ Markup.language_type
     (fn (syms, pos) =>
       parse_tree ctxt "type" (syms, pos)
       |> uncurry (report_result ctxt pos)
@@ -389,7 +389,7 @@
       else (Markup.language_term, "term", Config.get ctxt Syntax.root, I);
     val decode = constrain o Term_XML.Decode.term;
   in
-    Syntax.parse_token ctxt decode markup
+    Syntax.parse_input ctxt decode markup
       (fn (syms, pos) =>
         let
           val (ambig_msgs, results) = parse_tree ctxt root (syms, pos) ||> map (decode_term ctxt);
@@ -463,7 +463,7 @@
           else decode_appl ps asts
       | decode ps (Ast.Appl asts) = decode_appl ps asts;
 
-    val source = Syntax.read_token str;
+    val source = Syntax.read_input str;
     val pos = Input.pos_of source;
     val syms = Input.source_explode source;
     val ast =
diff -r f19f4afa49e2 -r d453c69596cc src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon Mar 23 23:16:40 2015 +0100
+++ b/src/Tools/Code/code_thingol.ML	Tue Mar 24 11:53:18 2015 +0100
@@ -895,7 +895,7 @@
       (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy');
     fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');
     fun read_const_expr str =
-      (case Syntax.parse_token ctxt (K NONE) (K Markup.empty) (SOME o Symbol_Pos.implode o #1) str of
+      (case Syntax.parse_input ctxt (K NONE) (K Markup.empty) (SOME o Symbol_Pos.implode o #1) str of
         SOME "_" => ([], consts_of thy)
       | SOME s =>
           if String.isSuffix "._" s
@@ -910,7 +910,7 @@
   let
     val (consts, consts_permissive) = read_const_exprs_internal ctxt const_exprs;
     val consts' = implemented_deps
-      (consts_program_permissive ((Proof_Context.theory_of ctxt)) consts_permissive);
+      (consts_program_permissive (Proof_Context.theory_of ctxt) consts_permissive);
   in union (op =) consts' consts end;
 
 
diff -r f19f4afa49e2 -r d453c69596cc src/Tools/induct_tacs.ML
--- a/src/Tools/induct_tacs.ML	Mon Mar 23 23:16:40 2015 +0100
+++ b/src/Tools/induct_tacs.ML	Tue Mar 24 11:53:18 2015 +0100
@@ -35,7 +35,7 @@
       | NONE =>
           (case Induct.find_casesT ctxt
               (#2 (check_type ctxt (Proof_Context.read_term_schematic ctxt s,
-                Syntax.read_token_pos s))) of
+                Syntax.read_input_pos s))) of
             rule :: _ => rule
           | [] => @{thm case_split}));
     val _ = Method.trace ctxt [rule];
@@ -72,7 +72,7 @@
     fun induct_var name =
       let
         val t = Syntax.read_term ctxt name;
-        val pos = Syntax.read_token_pos name;
+        val pos = Syntax.read_input_pos name;
         val (x, _) = Term.dest_Free t handle TERM _ =>
           error ("Induction argument not a variable: " ^
             quote (Syntax.string_of_term ctxt t) ^ Position.here pos);