Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/RAW/ml_positions.ML
changeset 61925 ab52f183f020
parent 56437 b14bd153a753 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/ml_positions.ML	Wed Dec 23 23:09:13 2015 +0100
@@ -0,0 +1,16 @@
+(*  Title:      Pure/RAW/ml_positions.ML
+    Author:     Makarius
+
+Approximate ML antiquotation @{here} for Isabelle/Pure bootstrap.
+*)
+
+fun ml_positions start_line name txt =
+  let
+    fun positions line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res =
+          let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")"
+          in positions line cs (s :: res) end
+      | positions line (c :: cs) res =
+          positions (if c = #"\n" then line + 1 else line) cs (str c :: res)
+      | positions _ [] res = rev res;
+  in String.concat (positions start_line (String.explode txt) []) end;
+
isabelle