1.1 --- a/src/Pure/Concurrent/future.ML Mon Jul 05 10:42:27 2010 +0200
1.2 +++ b/src/Pure/Concurrent/future.ML Mon Jul 05 10:47:39 2010 +0200
1.3 @@ -59,6 +59,7 @@
1.4 val cancel_group: group -> unit
1.5 val cancel: 'a future -> unit
1.6 val shutdown: unit -> unit
1.7 + val report: (unit -> 'a) -> 'a
1.8 end;
1.9
1.10 structure Future: FUTURE =
1.11 @@ -284,7 +285,7 @@
1.12 if forall (Thread.isActive o #1) (! workers) then ()
1.13 else
1.14 let
1.15 - val (alive, dead) = List.partition (Thread.isActive o #1) (! workers);
1.16 + val (alive, dead) = List.partition (Thread.isActive o #1) (! workers);
1.17 val _ = workers := alive;
1.18 in
1.19 Multithreading.tracing 0 (fn () =>
1.20 @@ -523,6 +524,16 @@
1.21 else ();
1.22
1.23
1.24 +(* report markup *)
1.25 +
1.26 +fun report e =
1.27 + let
1.28 + val _ = Output.status (Markup.markup Markup.forked "");
1.29 + val x = e (); (*sic -- report "joined" only for success*)
1.30 + val _ = Output.status (Markup.markup Markup.joined "");
1.31 + in x end;
1.32 +
1.33 +
1.34 (*final declarations of this structure!*)
1.35 val map = map_future;
1.36
2.1 --- a/src/Pure/Isar/toplevel.ML Mon Jul 05 10:42:27 2010 +0200
2.2 +++ b/src/Pure/Isar/toplevel.ML Mon Jul 05 10:47:39 2010 +0200
2.3 @@ -86,9 +86,9 @@
2.4 val error_msg: transition -> exn * string -> unit
2.5 val add_hook: (transition -> state -> state -> unit) -> unit
2.6 val transition: bool -> transition -> state -> (state * (exn * string) option) option
2.7 + val run_command: string -> transition -> state -> state option
2.8 val commit_exit: Position.T -> transition
2.9 val command: transition -> state -> state
2.10 - val run_command: string -> transition -> state -> state option
2.11 val excursion: (transition * transition list) list -> (transition * state) list lazy
2.12 end;
2.13
2.14 @@ -561,6 +561,12 @@
2.15 fun status tr m =
2.16 setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) ();
2.17
2.18 +fun async_state (tr as Transition {print, ...}) st =
2.19 + if print then
2.20 + ignore (Future.fork_group (Task_Queue.new_group (Future.worker_group ()))
2.21 + (fn () => Future.report (setmp_thread_position tr (fn () => print_state false st))))
2.22 + else ();
2.23 +
2.24 fun error_msg tr exn_info =
2.25 setmp_thread_position tr (fn () =>
2.26 Output.error_msg (ML_Compiler.exn_message (EXCURSION_FAIL exn_info))) ();
2.27 @@ -614,6 +620,22 @@
2.28 end;
2.29
2.30
2.31 +(* managed execution *)
2.32 +
2.33 +fun run_command thy_name (tr as Transition {print, ...}) st =
2.34 + (case
2.35 + (case init_of tr of
2.36 + SOME name => Exn.capture (fn () => Thy_Load.check_name thy_name name) ()
2.37 + | NONE => Exn.Result ()) of
2.38 + Exn.Result () =>
2.39 + (case transition false tr st of
2.40 + SOME (st', NONE) => (status tr Markup.finished; async_state tr st'; SOME st')
2.41 + | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn
2.42 + | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
2.43 + | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE))
2.44 + | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));
2.45 +
2.46 +
2.47 (* commit final exit *)
2.48
2.49 fun commit_exit pos =
2.50 @@ -635,19 +657,6 @@
2.51 let val st' = command tr st
2.52 in (st', st') end;
2.53
2.54 -fun run_command thy_name tr st =
2.55 - (case
2.56 - (case init_of tr of
2.57 - SOME name => Exn.capture (fn () => Thy_Load.check_name thy_name name) ()
2.58 - | NONE => Exn.Result ()) of
2.59 - Exn.Result () =>
2.60 - (case transition true tr st of
2.61 - SOME (st', NONE) => (status tr Markup.finished; SOME st')
2.62 - | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn
2.63 - | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
2.64 - | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE))
2.65 - | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));
2.66 -
2.67
2.68 (* excursion of units, consisting of commands with proof *)
2.69
3.1 --- a/src/Pure/PIDE/document.scala Mon Jul 05 10:42:27 2010 +0200
3.2 +++ b/src/Pure/PIDE/document.scala Mon Jul 05 10:47:39 2010 +0200
3.3 @@ -14,13 +14,13 @@
3.4 {
3.5 /* command start positions */
3.6
3.7 - def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] =
3.8 + def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] =
3.9 {
3.10 - var offset = 0
3.11 - for (cmd <- commands.iterator) yield {
3.12 - val start = offset
3.13 - offset += cmd.length
3.14 - (cmd, start)
3.15 + var i = offset
3.16 + for (command <- commands) yield {
3.17 + val start = i
3.18 + i += command.length
3.19 + (command, start)
3.20 }
3.21 }
3.22
3.23 @@ -60,9 +60,10 @@
3.24 {
3.25 eds match {
3.26 case e :: es =>
3.27 - command_starts(commands).find { // FIXME relative search!
3.28 + command_starts(commands.iterator).find {
3.29 case (cmd, cmd_start) =>
3.30 - e.can_edit(cmd.source, cmd_start) || e.is_insert && e.start == cmd_start + cmd.length
3.31 + e.can_edit(cmd.source, cmd_start) ||
3.32 + e.is_insert && e.start == cmd_start + cmd.length
3.33 } match {
3.34 case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
3.35 val (rest, text) = e.edit(cmd.source, cmd_start)
3.36 @@ -144,7 +145,7 @@
3.37 {
3.38 /* command ranges */
3.39
3.40 - def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands)
3.41 + def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands.iterator)
3.42
3.43 def command_start(cmd: Command): Option[Int] =
3.44 command_starts.find(_._1 == cmd).map(_._2)
4.1 --- a/src/Pure/Syntax/parser.ML Mon Jul 05 10:42:27 2010 +0200
4.2 +++ b/src/Pure/Syntax/parser.ML Mon Jul 05 10:47:39 2010 +0200
4.3 @@ -8,9 +8,9 @@
4.4 sig
4.5 type gram
4.6 val empty_gram: gram
4.7 - val extend_gram: gram -> Syn_Ext.xprod list -> gram
4.8 + val extend_gram: Syn_Ext.xprod list -> gram -> gram
4.9 val make_gram: Syn_Ext.xprod list -> gram
4.10 - val merge_grams: gram -> gram -> gram
4.11 + val merge_gram: gram * gram -> gram
4.12 val pretty_gram: gram -> Pretty.T list
4.13 datatype parsetree =
4.14 Node of string * parsetree list |
4.15 @@ -23,19 +23,16 @@
4.16 structure Parser: PARSER =
4.17 struct
4.18
4.19 -open Lexicon Syn_Ext;
4.20 -
4.21 -
4.22 (** datatype gram **)
4.23
4.24 type nt_tag = int; (*production for the NTs are stored in an array
4.25 so we can identify NTs by their index*)
4.26
4.27 -datatype symb = Terminal of token
4.28 +datatype symb = Terminal of Lexicon.token
4.29 | Nonterminal of nt_tag * int; (*(tag, precedence)*)
4.30
4.31 -type nt_gram = ((nt_tag list * token list) *
4.32 - (token option * (symb list * string * int) list) list);
4.33 +type nt_gram = ((nt_tag list * Lexicon.token list) *
4.34 + (Lexicon.token option * (symb list * string * int) list) list);
4.35 (*(([dependent_nts], [start_tokens]),
4.36 [(start_token, [(rhs, name, prio)])])*)
4.37 (*depent_nts is a list of all NTs whose lookahead
4.38 @@ -53,8 +50,8 @@
4.39 lambda productions are stored as normal productions
4.40 and also as an entry in "lambdas"*)
4.41
4.42 -val UnknownStart = eof; (*productions for which no starting token is
4.43 - known yet are associated with this token*)
4.44 +val UnknownStart = Lexicon.eof; (*productions for which no starting token is
4.45 + known yet are associated with this token*)
4.46
4.47 (* get all NTs that are connected with a list of NTs
4.48 (used for expanding chain list)*)
4.49 @@ -125,7 +122,7 @@
4.50 (*get all known starting tokens for a nonterminal*)
4.51 fun starts_for_nt nt = snd (fst (Array.sub (prods, nt)));
4.52
4.53 - val token_union = uncurry (union matching_tokens);
4.54 + val token_union = uncurry (union Lexicon.matching_tokens);
4.55
4.56 (*update prods, lookaheads, and lambdas according to new lambda NTs*)
4.57 val (added_starts', lambdas') =
4.58 @@ -158,7 +155,7 @@
4.59 val nt_dependencies' = union (op =) nts nt_dependencies;
4.60
4.61 (*associate production with new starting tokens*)
4.62 - fun copy ([]: token option list) nt_prods = nt_prods
4.63 + fun copy ([]: Lexicon.token option list) nt_prods = nt_prods
4.64 | copy (tk :: tks) nt_prods =
4.65 let val old_prods = these (AList.lookup (op =) nt_prods tk);
4.66
4.67 @@ -259,7 +256,7 @@
4.68 let
4.69 val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt);
4.70
4.71 - val new_tks = subtract matching_tokens old_tks start_tks;
4.72 + val new_tks = subtract Lexicon.matching_tokens old_tks start_tks;
4.73
4.74 (*store new production*)
4.75 fun store [] prods is_new =
4.76 @@ -278,7 +275,7 @@
4.77 else (new_prod :: tk_prods, true);
4.78
4.79 val prods' = prods
4.80 - |> is_new' ? AList.update (op =) (tk: token option, tk_prods');
4.81 + |> is_new' ? AList.update (op =) (tk: Lexicon.token option, tk_prods');
4.82 in store tks prods' (is_new orelse is_new') end;
4.83
4.84 val (nt_prods', prod_count', changed) =
4.85 @@ -329,10 +326,10 @@
4.86 andalso member (op =) new_tks (the tk);
4.87
4.88 (*associate production with new starting tokens*)
4.89 - fun copy ([]: token list) nt_prods = nt_prods
4.90 + fun copy ([]: Lexicon.token list) nt_prods = nt_prods
4.91 | copy (tk :: tks) nt_prods =
4.92 let
4.93 - val tk_prods = (these o AList.lookup (op =) nt_prods) (SOME tk);
4.94 + val tk_prods = these (AList.lookup (op =) nt_prods (SOME tk));
4.95
4.96 val tk_prods' =
4.97 if not lambda then p :: tk_prods
4.98 @@ -359,7 +356,7 @@
4.99 val (lookahead as (old_nts, old_tks), nt_prods) =
4.100 Array.sub (prods, nt);
4.101
4.102 - val tk_prods = (these o AList.lookup (op =) nt_prods) key;
4.103 + val tk_prods = these (AList.lookup (op =) nt_prods key);
4.104
4.105 (*associate productions with new lookahead tokens*)
4.106 val (tk_prods', nt_prods') =
4.107 @@ -370,7 +367,7 @@
4.108 |> (key = SOME UnknownStart) ? AList.update (op =) (key, tk_prods')
4.109
4.110 val added_tks =
4.111 - subtract matching_tokens old_tks new_tks;
4.112 + subtract Lexicon.matching_tokens old_tks new_tks;
4.113 in if null added_tks then
4.114 (Array.update (prods, nt, (lookahead, nt_prods'));
4.115 process_nts nts added)
4.116 @@ -381,7 +378,7 @@
4.117 end;
4.118
4.119 val ((dependent, _), _) = Array.sub (prods, changed_nt);
4.120 - in add_starts (starts @ (process_nts dependent [])) end;
4.121 + in add_starts (starts @ process_nts dependent []) end;
4.122 in add_starts added_starts' end;
4.123 in add_prods prods chains' lambdas' prod_count ps end;
4.124
4.125 @@ -394,8 +391,8 @@
4.126
4.127 val nt_name = the o Inttab.lookup (Inttab.make (map swap (Symtab.dest tags)));
4.128
4.129 - fun pretty_symb (Terminal (Token (Literal, s, _))) = Pretty.quote (Pretty.str s)
4.130 - | pretty_symb (Terminal tok) = Pretty.str (str_of_token tok)
4.131 + fun pretty_symb (Terminal (Lexicon.Token (Lexicon.Literal, s, _))) = Pretty.quote (Pretty.str s)
4.132 + | pretty_symb (Terminal tok) = Pretty.str (Lexicon.str_of_token tok)
4.133 | pretty_symb (Nonterminal (tag, p)) =
4.134 Pretty.str (nt_name tag ^ "[" ^ signed_string_of_int p ^ "]");
4.135
4.136 @@ -422,7 +419,6 @@
4.137
4.138 (** Operations on gramars **)
4.139
4.140 -(*The mother of all grammars*)
4.141 val empty_gram = Gram {nt_count = 0, prod_count = 0,
4.142 tags = Symtab.empty, chains = [], lambdas = [],
4.143 prods = Array.array (0, (([], []), []))};
4.144 @@ -439,75 +435,75 @@
4.145
4.146
4.147 (*Add productions to a grammar*)
4.148 -fun extend_gram gram [] = gram
4.149 - | extend_gram (Gram {nt_count, prod_count, tags, chains, lambdas, prods})
4.150 - xprods =
4.151 - let
4.152 - (*Get tag for existing nonterminal or create a new one*)
4.153 - fun get_tag nt_count tags nt =
4.154 - case Symtab.lookup tags nt of
4.155 - SOME tag => (nt_count, tags, tag)
4.156 - | NONE => (nt_count+1, Symtab.update_new (nt, nt_count) tags,
4.157 - nt_count);
4.158 +fun extend_gram [] gram = gram
4.159 + | extend_gram xprods (Gram {nt_count, prod_count, tags, chains, lambdas, prods}) =
4.160 + let
4.161 + (*Get tag for existing nonterminal or create a new one*)
4.162 + fun get_tag nt_count tags nt =
4.163 + case Symtab.lookup tags nt of
4.164 + SOME tag => (nt_count, tags, tag)
4.165 + | NONE => (nt_count+1, Symtab.update_new (nt, nt_count) tags,
4.166 + nt_count);
4.167
4.168 - (*Convert symbols to the form used by the parser;
4.169 - delimiters and predefined terms are stored as terminals,
4.170 - nonterminals are converted to integer tags*)
4.171 - fun symb_of [] nt_count tags result = (nt_count, tags, rev result)
4.172 - | symb_of ((Delim s) :: ss) nt_count tags result =
4.173 - symb_of ss nt_count tags (Terminal (Token (Literal, s, Position.no_range)) :: result)
4.174 - | symb_of ((Argument (s, p)) :: ss) nt_count tags result =
4.175 - let
4.176 - val (nt_count', tags', new_symb) =
4.177 - case predef_term s of
4.178 - NONE =>
4.179 - let val (nt_count', tags', s_tag) = get_tag nt_count tags s;
4.180 - in (nt_count', tags', Nonterminal (s_tag, p)) end
4.181 - | SOME tk => (nt_count, tags, Terminal tk);
4.182 - in symb_of ss nt_count' tags' (new_symb :: result) end
4.183 - | symb_of (_ :: ss) nt_count tags result =
4.184 - symb_of ss nt_count tags result;
4.185 + (*Convert symbols to the form used by the parser;
4.186 + delimiters and predefined terms are stored as terminals,
4.187 + nonterminals are converted to integer tags*)
4.188 + fun symb_of [] nt_count tags result = (nt_count, tags, rev result)
4.189 + | symb_of ((Syn_Ext.Delim s) :: ss) nt_count tags result =
4.190 + symb_of ss nt_count tags
4.191 + (Terminal (Lexicon.Token (Lexicon.Literal, s, Position.no_range)) :: result)
4.192 + | symb_of ((Syn_Ext.Argument (s, p)) :: ss) nt_count tags result =
4.193 + let
4.194 + val (nt_count', tags', new_symb) =
4.195 + case Lexicon.predef_term s of
4.196 + NONE =>
4.197 + let val (nt_count', tags', s_tag) = get_tag nt_count tags s;
4.198 + in (nt_count', tags', Nonterminal (s_tag, p)) end
4.199 + | SOME tk => (nt_count, tags, Terminal tk);
4.200 + in symb_of ss nt_count' tags' (new_symb :: result) end
4.201 + | symb_of (_ :: ss) nt_count tags result =
4.202 + symb_of ss nt_count tags result;
4.203
4.204 - (*Convert list of productions by invoking symb_of for each of them*)
4.205 - fun prod_of [] nt_count prod_count tags result =
4.206 - (nt_count, prod_count, tags, result)
4.207 - | prod_of ((XProd (lhs, xsymbs, const, pri)) :: ps)
4.208 - nt_count prod_count tags result =
4.209 - let val (nt_count', tags', lhs_tag) = get_tag nt_count tags lhs;
4.210 + (*Convert list of productions by invoking symb_of for each of them*)
4.211 + fun prod_of [] nt_count prod_count tags result =
4.212 + (nt_count, prod_count, tags, result)
4.213 + | prod_of ((Syn_Ext.XProd (lhs, xsymbs, const, pri)) :: ps)
4.214 + nt_count prod_count tags result =
4.215 + let val (nt_count', tags', lhs_tag) = get_tag nt_count tags lhs;
4.216
4.217 - val (nt_count'', tags'', prods) =
4.218 - symb_of xsymbs nt_count' tags' [];
4.219 - in prod_of ps nt_count'' (prod_count+1) tags''
4.220 - ((lhs_tag, (prods, const, pri)) :: result)
4.221 - end;
4.222 + val (nt_count'', tags'', prods) =
4.223 + symb_of xsymbs nt_count' tags' [];
4.224 + in prod_of ps nt_count'' (prod_count+1) tags''
4.225 + ((lhs_tag, (prods, const, pri)) :: result)
4.226 + end;
4.227
4.228 - val (nt_count', prod_count', tags', xprods') =
4.229 - prod_of xprods nt_count prod_count tags [];
4.230 + val (nt_count', prod_count', tags', xprods') =
4.231 + prod_of xprods nt_count prod_count tags [];
4.232
4.233 - (*Copy array containing productions of old grammar;
4.234 - this has to be done to preserve the old grammar while being able
4.235 - to change the array's content*)
4.236 - val prods' =
4.237 - let fun get_prod i = if i < nt_count then Array.sub (prods, i)
4.238 - else (([], []), []);
4.239 - in Array.tabulate (nt_count', get_prod) end;
4.240 + (*Copy array containing productions of old grammar;
4.241 + this has to be done to preserve the old grammar while being able
4.242 + to change the array's content*)
4.243 + val prods' =
4.244 + let fun get_prod i = if i < nt_count then Array.sub (prods, i)
4.245 + else (([], []), []);
4.246 + in Array.tabulate (nt_count', get_prod) end;
4.247
4.248 - val fromto_chains = inverse_chains chains [];
4.249 + val fromto_chains = inverse_chains chains [];
4.250
4.251 - (*Add new productions to old ones*)
4.252 - val (fromto_chains', lambdas', _) =
4.253 - add_prods prods' fromto_chains lambdas NONE xprods';
4.254 + (*Add new productions to old ones*)
4.255 + val (fromto_chains', lambdas', _) =
4.256 + add_prods prods' fromto_chains lambdas NONE xprods';
4.257
4.258 - val chains' = inverse_chains fromto_chains' [];
4.259 - in Gram {nt_count = nt_count', prod_count = prod_count', tags = tags',
4.260 - chains = chains', lambdas = lambdas', prods = prods'}
4.261 - end;
4.262 + val chains' = inverse_chains fromto_chains' [];
4.263 + in Gram {nt_count = nt_count', prod_count = prod_count', tags = tags',
4.264 + chains = chains', lambdas = lambdas', prods = prods'}
4.265 + end;
4.266
4.267 -val make_gram = extend_gram empty_gram;
4.268 +fun make_gram xprods = extend_gram xprods empty_gram;
4.269
4.270
4.271 (*Merge two grammars*)
4.272 -fun merge_grams gram_a gram_b =
4.273 +fun merge_gram (gram_a, gram_b) =
4.274 let
4.275 (*find out which grammar is bigger*)
4.276 val (Gram {nt_count = nt_count1, prod_count = prod_count1, tags = tags1,
4.277 @@ -604,7 +600,7 @@
4.278
4.279 datatype parsetree =
4.280 Node of string * parsetree list |
4.281 - Tip of token;
4.282 + Tip of Lexicon.token;
4.283
4.284 type state =
4.285 nt_tag * int * (*identification and production precedence*)
4.286 @@ -675,7 +671,7 @@
4.287
4.288
4.289 fun movedot_term (A, j, ts, Terminal a :: sa, id, i) c =
4.290 - if valued_token c then
4.291 + if Lexicon.valued_token c then
4.292 (A, j, ts @ [Tip c], sa, id, i)
4.293 else (A, j, ts, sa, id, i);
4.294
4.295 @@ -695,105 +691,105 @@
4.296 (*get all productions of a NT and NTs chained to it which can
4.297 be started by specified token*)
4.298 fun prods_for prods chains include_none tk nts =
4.299 -let
4.300 - fun token_assoc (list, key) =
4.301 - let fun assoc [] result = result
4.302 - | assoc ((keyi, pi) :: pairs) result =
4.303 - if is_some keyi andalso matching_tokens (the keyi, key)
4.304 - orelse include_none andalso is_none keyi then
4.305 - assoc pairs (pi @ result)
4.306 - else assoc pairs result;
4.307 - in assoc list [] end;
4.308 + let
4.309 + fun token_assoc (list, key) =
4.310 + let fun assoc [] result = result
4.311 + | assoc ((keyi, pi) :: pairs) result =
4.312 + if is_some keyi andalso Lexicon.matching_tokens (the keyi, key)
4.313 + orelse include_none andalso is_none keyi then
4.314 + assoc pairs (pi @ result)
4.315 + else assoc pairs result;
4.316 + in assoc list [] end;
4.317
4.318 - fun get_prods [] result = result
4.319 - | get_prods (nt :: nts) result =
4.320 - let val nt_prods = snd (Array.sub (prods, nt));
4.321 - in get_prods nts ((token_assoc (nt_prods, tk)) @ result) end;
4.322 -in get_prods (connected_with chains nts nts) [] end;
4.323 + fun get_prods [] result = result
4.324 + | get_prods (nt :: nts) result =
4.325 + let val nt_prods = snd (Array.sub (prods, nt));
4.326 + in get_prods nts ((token_assoc (nt_prods, tk)) @ result) end;
4.327 + in get_prods (connected_with chains nts nts) [] end;
4.328
4.329
4.330 fun PROCESSS warned prods chains Estate i c states =
4.331 -let
4.332 -fun all_prods_for nt = prods_for prods chains true c [nt];
4.333 + let
4.334 + fun all_prods_for nt = prods_for prods chains true c [nt];
4.335
4.336 -fun processS used [] (Si, Sii) = (Si, Sii)
4.337 - | processS used (S :: States) (Si, Sii) =
4.338 - (case S of
4.339 - (_, _, _, Nonterminal (nt, minPrec) :: _, _, _) =>
4.340 - let (*predictor operation*)
4.341 - val (used', new_states) =
4.342 - (case AList.lookup (op =) used nt of
4.343 - SOME (usedPrec, l) => (*nonterminal has been processed*)
4.344 - if usedPrec <= minPrec then
4.345 - (*wanted precedence has been processed*)
4.346 - (used, movedot_lambda S l)
4.347 - else (*wanted precedence hasn't been parsed yet*)
4.348 - let
4.349 - val tk_prods = all_prods_for nt;
4.350 + fun processS used [] (Si, Sii) = (Si, Sii)
4.351 + | processS used (S :: States) (Si, Sii) =
4.352 + (case S of
4.353 + (_, _, _, Nonterminal (nt, minPrec) :: _, _, _) =>
4.354 + let (*predictor operation*)
4.355 + val (used', new_states) =
4.356 + (case AList.lookup (op =) used nt of
4.357 + SOME (usedPrec, l) => (*nonterminal has been processed*)
4.358 + if usedPrec <= minPrec then
4.359 + (*wanted precedence has been processed*)
4.360 + (used, movedot_lambda S l)
4.361 + else (*wanted precedence hasn't been parsed yet*)
4.362 + let
4.363 + val tk_prods = all_prods_for nt;
4.364
4.365 - val States' = mkStates i minPrec nt
4.366 - (getRHS' minPrec usedPrec tk_prods);
4.367 - in (update_prec (nt, minPrec) used,
4.368 - movedot_lambda S l @ States')
4.369 - end
4.370 + val States' = mkStates i minPrec nt
4.371 + (getRHS' minPrec usedPrec tk_prods);
4.372 + in (update_prec (nt, minPrec) used,
4.373 + movedot_lambda S l @ States')
4.374 + end
4.375
4.376 - | NONE => (*nonterminal is parsed for the first time*)
4.377 - let val tk_prods = all_prods_for nt;
4.378 - val States' = mkStates i minPrec nt
4.379 - (getRHS minPrec tk_prods);
4.380 - in ((nt, (minPrec, [])) :: used, States') end);
4.381 + | NONE => (*nonterminal is parsed for the first time*)
4.382 + let val tk_prods = all_prods_for nt;
4.383 + val States' = mkStates i minPrec nt
4.384 + (getRHS minPrec tk_prods);
4.385 + in ((nt, (minPrec, [])) :: used, States') end);
4.386
4.387 - val dummy =
4.388 - if not (!warned) andalso
4.389 - length (new_states @ States) > (!branching_level) then
4.390 - (warning "Currently parsed expression could be extremely ambiguous.";
4.391 - warned := true)
4.392 - else ();
4.393 - in
4.394 - processS used' (new_states @ States) (S :: Si, Sii)
4.395 - end
4.396 - | (_, _, _, Terminal a :: _, _, _) => (*scanner operation*)
4.397 - processS used States
4.398 - (S :: Si,
4.399 - if matching_tokens (a, c) then movedot_term S c :: Sii else Sii)
4.400 - | (A, prec, ts, [], id, j) => (*completer operation*)
4.401 - let val tt = if id = "" then ts else [Node (id, ts)] in
4.402 - if j = i then (*lambda production?*)
4.403 - let
4.404 - val (used', O) = update_trees used (A, (tt, prec));
4.405 + val dummy =
4.406 + if not (!warned) andalso
4.407 + length (new_states @ States) > (!branching_level) then
4.408 + (warning "Currently parsed expression could be extremely ambiguous.";
4.409 + warned := true)
4.410 + else ();
4.411 in
4.412 - case O of
4.413 - NONE =>
4.414 - let val Slist = getS A prec Si;
4.415 - val States' = map (movedot_nonterm tt) Slist;
4.416 - in processS used' (States' @ States) (S :: Si, Sii) end
4.417 - | SOME n =>
4.418 - if n >= prec then processS used' States (S :: Si, Sii)
4.419 - else
4.420 - let val Slist = getS' A prec n Si;
4.421 - val States' = map (movedot_nonterm tt) Slist;
4.422 - in processS used' (States' @ States) (S :: Si, Sii) end
4.423 + processS used' (new_states @ States) (S :: Si, Sii)
4.424 end
4.425 - else
4.426 - let val Slist = getStates Estate i j A prec
4.427 - in processS used (map (movedot_nonterm tt) Slist @ States)
4.428 - (S :: Si, Sii)
4.429 - end
4.430 - end)
4.431 -in processS [] states ([], []) end;
4.432 + | (_, _, _, Terminal a :: _, _, _) => (*scanner operation*)
4.433 + processS used States
4.434 + (S :: Si,
4.435 + if Lexicon.matching_tokens (a, c) then movedot_term S c :: Sii else Sii)
4.436 + | (A, prec, ts, [], id, j) => (*completer operation*)
4.437 + let val tt = if id = "" then ts else [Node (id, ts)] in
4.438 + if j = i then (*lambda production?*)
4.439 + let
4.440 + val (used', O) = update_trees used (A, (tt, prec));
4.441 + in
4.442 + case O of
4.443 + NONE =>
4.444 + let val Slist = getS A prec Si;
4.445 + val States' = map (movedot_nonterm tt) Slist;
4.446 + in processS used' (States' @ States) (S :: Si, Sii) end
4.447 + | SOME n =>
4.448 + if n >= prec then processS used' States (S :: Si, Sii)
4.449 + else
4.450 + let val Slist = getS' A prec n Si;
4.451 + val States' = map (movedot_nonterm tt) Slist;
4.452 + in processS used' (States' @ States) (S :: Si, Sii) end
4.453 + end
4.454 + else
4.455 + let val Slist = getStates Estate i j A prec
4.456 + in processS used (map (movedot_nonterm tt) Slist @ States)
4.457 + (S :: Si, Sii)
4.458 + end
4.459 + end)
4.460 + in processS [] states ([], []) end;
4.461
4.462
4.463 fun produce warned prods tags chains stateset i indata prev_token =
4.464 (case Array.sub (stateset, i) of
4.465 [] =>
4.466 let
4.467 - val toks = if is_eof prev_token then indata else prev_token :: indata;
4.468 - val pos = Position.str_of (pos_of_token prev_token);
4.469 + val toks = if Lexicon.is_eof prev_token then indata else prev_token :: indata;
4.470 + val pos = Position.str_of (Lexicon.pos_of_token prev_token);
4.471 in
4.472 if null toks then error ("Inner syntax error: unexpected end of input" ^ pos)
4.473 else error (Pretty.string_of (Pretty.block
4.474 (Pretty.str ("Inner syntax error" ^ pos ^ " at \"") ::
4.475 - Pretty.breaks (map (Pretty.str o str_of_token) (#1 (split_last toks))) @
4.476 + Pretty.breaks (map (Pretty.str o Lexicon.str_of_token) (#1 (split_last toks))) @
4.477 [Pretty.str "\""])))
4.478 end
4.479 | s =>
4.480 @@ -807,21 +803,20 @@
4.481 end));
4.482
4.483
4.484 -fun get_trees l = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE)
4.485 - l;
4.486 +fun get_trees l = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) l;
4.487
4.488 fun earley prods tags chains startsymbol indata =
4.489 let
4.490 - val start_tag = case Symtab.lookup tags startsymbol of
4.491 - SOME tag => tag
4.492 - | NONE => error ("parse: Unknown startsymbol " ^
4.493 - quote startsymbol);
4.494 - val S0 = [(~1, 0, [], [Nonterminal (start_tag, 0), Terminal eof], "", 0)];
4.495 + val start_tag =
4.496 + (case Symtab.lookup tags startsymbol of
4.497 + SOME tag => tag
4.498 + | NONE => error ("Inner syntax: unknown startsymbol " ^ quote startsymbol));
4.499 + val S0 = [(~1, 0, [], [Nonterminal (start_tag, 0), Terminal Lexicon.eof], "", 0)];
4.500 val s = length indata + 1;
4.501 val Estate = Array.array (s, []);
4.502 in
4.503 Array.update (Estate, 0, S0);
4.504 - get_trees (produce (Unsynchronized.ref false) prods tags chains Estate 0 indata eof)
4.505 + get_trees (produce (Unsynchronized.ref false) prods tags chains Estate 0 indata Lexicon.eof)
4.506 end;
4.507
4.508
4.509 @@ -830,10 +825,10 @@
4.510 val end_pos =
4.511 (case try List.last toks of
4.512 NONE => Position.none
4.513 - | SOME (Token (_, _, (_, end_pos))) => end_pos);
4.514 + | SOME (Lexicon.Token (_, _, (_, end_pos))) => end_pos);
4.515 val r =
4.516 - (case earley prods tags chains start (toks @ [mk_eof end_pos]) of
4.517 - [] => sys_error "parse: no parse trees"
4.518 + (case earley prods tags chains start (toks @ [Lexicon.mk_eof end_pos]) of
4.519 + [] => raise Fail "no parse trees"
4.520 | pts => pts);
4.521 in r end;
4.522
4.523 @@ -842,7 +837,8 @@
4.524 let
4.525 fun freeze a = map_range (curry Array.sub a) (Array.length a);
4.526 val prods = maps snd (maps snd (freeze (#prods gram)));
4.527 - fun guess (SOME ([Nonterminal (_, k), Terminal (Token (Literal, s, _)), Nonterminal (_, l)], _, j)) =
4.528 + fun guess (SOME ([Nonterminal (_, k),
4.529 + Terminal (Lexicon.Token (Lexicon.Literal, s, _)), Nonterminal (_, l)], _, j)) =
4.530 if k = j andalso l = j + 1 then SOME (s, true, false, j)
4.531 else if k = j + 1 then if l = j then SOME (s, false, true, j)
4.532 else if l = j + 1 then SOME (s, false, false, j)
5.1 --- a/src/Pure/Syntax/syntax.ML Mon Jul 05 10:42:27 2010 +0200
5.2 +++ b/src/Pure/Syntax/syntax.ML Mon Jul 05 10:47:39 2010 +0200
5.3 @@ -297,7 +297,7 @@
5.4 Syntax
5.5 ({input = new_xprods @ input,
5.6 lexicon = fold Scan.extend_lexicon (Syn_Ext.delims_of new_xprods) lexicon,
5.7 - gram = Parser.extend_gram gram new_xprods,
5.8 + gram = Parser.extend_gram new_xprods gram,
5.9 consts = Library.merge (op =) (consts1, filter_out Lexicon.is_marked consts2),
5.10 prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
5.11 parse_ast_trtab =
5.12 @@ -362,7 +362,7 @@
5.13 Syntax
5.14 ({input = Library.merge (op =) (input1, input2),
5.15 lexicon = Scan.merge_lexicons (lexicon1, lexicon2),
5.16 - gram = Parser.merge_grams gram1 gram2,
5.17 + gram = Parser.merge_gram (gram1, gram2),
5.18 consts = sort_distinct string_ord (consts1 @ consts2),
5.19 prmodes = Library.merge (op =) (prmodes1, prmodes2),
5.20 parse_ast_trtab =
6.1 --- a/src/Pure/System/isabelle_process.ML Mon Jul 05 10:42:27 2010 +0200
6.2 +++ b/src/Pure/System/isabelle_process.ML Mon Jul 05 10:47:39 2010 +0200
6.3 @@ -91,6 +91,7 @@
6.4 (Unsynchronized.change print_mode
6.5 (fold (update op =) [isabelle_processN, Keyword.keyword_status_reportN, Pretty.symbolicN]);
6.6 setup_channels out |> init_message;
6.7 + quick_and_dirty := true; (* FIXME !? *)
6.8 Keyword.report ();
6.9 Output.status (Markup.markup Markup.ready "");
6.10 Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
7.1 --- a/src/Pure/System/isabelle_process.scala Mon Jul 05 10:42:27 2010 +0200
7.2 +++ b/src/Pure/System/isabelle_process.scala Mon Jul 05 10:47:39 2010 +0200
7.3 @@ -19,89 +19,55 @@
7.4 {
7.5 /* results */
7.6
7.7 - object Kind extends Enumeration {
7.8 - //{{{ values and codes
7.9 - // internal system notification
7.10 - val SYSTEM = Value("SYSTEM")
7.11 - // Posix channels/events
7.12 - val STDIN = Value("STDIN")
7.13 - val STDOUT = Value("STDOUT")
7.14 - val SIGNAL = Value("SIGNAL")
7.15 - val EXIT = Value("EXIT")
7.16 - // Isabelle messages
7.17 - val INIT = Value("INIT")
7.18 - val STATUS = Value("STATUS")
7.19 - val WRITELN = Value("WRITELN")
7.20 - val TRACING = Value("TRACING")
7.21 - val WARNING = Value("WARNING")
7.22 - val ERROR = Value("ERROR")
7.23 - val DEBUG = Value("DEBUG")
7.24 - // messages codes
7.25 - val code = Map(
7.26 - ('A' : Int) -> Kind.INIT,
7.27 - ('B' : Int) -> Kind.STATUS,
7.28 - ('C' : Int) -> Kind.WRITELN,
7.29 - ('D' : Int) -> Kind.TRACING,
7.30 - ('E' : Int) -> Kind.WARNING,
7.31 - ('F' : Int) -> Kind.ERROR,
7.32 - ('G' : Int) -> Kind.DEBUG,
7.33 - ('0' : Int) -> Kind.SYSTEM,
7.34 - ('1' : Int) -> Kind.STDIN,
7.35 - ('2' : Int) -> Kind.STDOUT,
7.36 - ('3' : Int) -> Kind.SIGNAL,
7.37 - ('4' : Int) -> Kind.EXIT)
7.38 + object Kind {
7.39 // message markup
7.40 val markup = Map(
7.41 - Kind.INIT -> Markup.INIT,
7.42 - Kind.STATUS -> Markup.STATUS,
7.43 - Kind.WRITELN -> Markup.WRITELN,
7.44 - Kind.TRACING -> Markup.TRACING,
7.45 - Kind.WARNING -> Markup.WARNING,
7.46 - Kind.ERROR -> Markup.ERROR,
7.47 - Kind.DEBUG -> Markup.DEBUG,
7.48 - Kind.SYSTEM -> Markup.SYSTEM,
7.49 - Kind.STDIN -> Markup.STDIN,
7.50 - Kind.STDOUT -> Markup.STDOUT,
7.51 - Kind.SIGNAL -> Markup.SIGNAL,
7.52 - Kind.EXIT -> Markup.EXIT)
7.53 - //}}}
7.54 - def is_raw(kind: Value) =
7.55 - kind == STDOUT
7.56 - def is_control(kind: Value) =
7.57 - kind == SYSTEM ||
7.58 - kind == SIGNAL ||
7.59 - kind == EXIT
7.60 - def is_system(kind: Value) =
7.61 - kind == SYSTEM ||
7.62 - kind == STDIN ||
7.63 - kind == SIGNAL ||
7.64 - kind == EXIT ||
7.65 - kind == STATUS
7.66 + ('A' : Int) -> Markup.INIT,
7.67 + ('B' : Int) -> Markup.STATUS,
7.68 + ('C' : Int) -> Markup.WRITELN,
7.69 + ('D' : Int) -> Markup.TRACING,
7.70 + ('E' : Int) -> Markup.WARNING,
7.71 + ('F' : Int) -> Markup.ERROR,
7.72 + ('G' : Int) -> Markup.DEBUG)
7.73 + def is_raw(kind: String) =
7.74 + kind == Markup.STDOUT
7.75 + def is_control(kind: String) =
7.76 + kind == Markup.SYSTEM ||
7.77 + kind == Markup.SIGNAL ||
7.78 + kind == Markup.EXIT
7.79 + def is_system(kind: String) =
7.80 + kind == Markup.SYSTEM ||
7.81 + kind == Markup.STDIN ||
7.82 + kind == Markup.SIGNAL ||
7.83 + kind == Markup.EXIT ||
7.84 + kind == Markup.STATUS
7.85 }
7.86
7.87 - class Result(val kind: Kind.Value, val props: List[(String, String)], val body: List[XML.Tree])
7.88 + class Result(val message: XML.Elem)
7.89 {
7.90 - def message = XML.Elem(Kind.markup(kind), props, body)
7.91 + def kind = message.name
7.92 + def body = message.body
7.93 +
7.94 + def is_raw = Kind.is_raw(kind)
7.95 + def is_control = Kind.is_control(kind)
7.96 + def is_system = Kind.is_system(kind)
7.97 + def is_status = kind == Markup.STATUS
7.98 + def is_ready = is_status && body == List(XML.Elem(Markup.READY, Nil, Nil))
7.99
7.100 override def toString: String =
7.101 {
7.102 val res =
7.103 - if (kind == Kind.STATUS) body.map(_.toString).mkString
7.104 - else Pretty.string_of(body)
7.105 + if (is_status) message.body.map(_.toString).mkString
7.106 + else Pretty.string_of(message.body)
7.107 + val props = message.attributes
7.108 if (props.isEmpty)
7.109 kind.toString + " [[" + res + "]]"
7.110 else
7.111 kind.toString + " " +
7.112 (for ((x, y) <- props) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
7.113 }
7.114 - def is_raw = Kind.is_raw(kind)
7.115 - def is_control = Kind.is_control(kind)
7.116 - def is_system = Kind.is_system(kind)
7.117
7.118 - def is_ready = kind == Kind.STATUS && body == List(XML.Elem(Markup.READY, Nil, Nil))
7.119 -
7.120 - def cache(c: XML.Cache): Result =
7.121 - new Result(kind, c.cache_props(props), c.cache_trees(body))
7.122 + def cache(c: XML.Cache): Result = new Result(c.cache_tree(message).asInstanceOf[XML.Elem])
7.123 }
7.124 }
7.125
7.126 @@ -127,15 +93,15 @@
7.127
7.128 /* results */
7.129
7.130 - private def put_result(kind: Kind.Value, props: List[(String, String)], body: List[XML.Tree])
7.131 + private def put_result(kind: String, props: List[(String, String)], body: List[XML.Tree])
7.132 {
7.133 - if (kind == Kind.INIT) {
7.134 + if (kind == Markup.INIT) {
7.135 for ((Markup.PID, p) <- props) pid = p
7.136 }
7.137 - receiver ! new Result(kind, props, body)
7.138 + receiver ! new Result(XML.Elem(kind, props, body))
7.139 }
7.140
7.141 - private def put_result(kind: Kind.Value, text: String)
7.142 + private def put_result(kind: String, text: String)
7.143 {
7.144 put_result(kind, Nil, List(XML.Text(system.symbols.decode(text))))
7.145 }
7.146 @@ -145,13 +111,13 @@
7.147
7.148 def interrupt() = synchronized {
7.149 if (proc == null) error("Cannot interrupt Isabelle: no process")
7.150 - if (pid == null) put_result(Kind.SYSTEM, "Cannot interrupt: unknown pid")
7.151 + if (pid == null) put_result(Markup.SYSTEM, "Cannot interrupt: unknown pid")
7.152 else {
7.153 try {
7.154 if (system.execute(true, "kill", "-INT", pid).waitFor == 0)
7.155 - put_result(Kind.SIGNAL, "INT")
7.156 + put_result(Markup.SIGNAL, "INT")
7.157 else
7.158 - put_result(Kind.SYSTEM, "Cannot interrupt: kill command failed")
7.159 + put_result(Markup.SYSTEM, "Cannot interrupt: kill command failed")
7.160 }
7.161 catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
7.162 }
7.163 @@ -162,7 +128,7 @@
7.164 else {
7.165 try_close()
7.166 Thread.sleep(500) // FIXME property!?
7.167 - put_result(Kind.SIGNAL, "KILL")
7.168 + put_result(Markup.SIGNAL, "KILL")
7.169 proc.destroy
7.170 proc = null
7.171 pid = null
7.172 @@ -222,17 +188,17 @@
7.173 finished = true
7.174 }
7.175 else {
7.176 - put_result(Kind.STDIN, s)
7.177 + put_result(Markup.STDIN, s)
7.178 writer.write(s)
7.179 writer.flush
7.180 }
7.181 //}}}
7.182 }
7.183 catch {
7.184 - case e: IOException => put_result(Kind.SYSTEM, "Stdin thread: " + e.getMessage)
7.185 + case e: IOException => put_result(Markup.SYSTEM, "Stdin thread: " + e.getMessage)
7.186 }
7.187 }
7.188 - put_result(Kind.SYSTEM, "Stdin thread terminated")
7.189 + put_result(Markup.SYSTEM, "Stdin thread terminated")
7.190 }
7.191 }
7.192
7.193 @@ -256,7 +222,7 @@
7.194 else done = true
7.195 }
7.196 if (result.length > 0) {
7.197 - put_result(Kind.STDOUT, result.toString)
7.198 + put_result(Markup.STDOUT, result.toString)
7.199 result.length = 0
7.200 }
7.201 else {
7.202 @@ -267,10 +233,10 @@
7.203 //}}}
7.204 }
7.205 catch {
7.206 - case e: IOException => put_result(Kind.SYSTEM, "Stdout thread: " + e.getMessage)
7.207 + case e: IOException => put_result(Markup.SYSTEM, "Stdout thread: " + e.getMessage)
7.208 }
7.209 }
7.210 - put_result(Kind.SYSTEM, "Stdout thread terminated")
7.211 + put_result(Markup.SYSTEM, "Stdout thread terminated")
7.212 }
7.213 }
7.214
7.215 @@ -332,8 +298,8 @@
7.216 val body = read_chunk()
7.217 header match {
7.218 case List(XML.Elem(name, props, Nil))
7.219 - if name.size == 1 && Kind.code.isDefinedAt(name(0)) =>
7.220 - put_result(Kind.code(name(0)), props, body)
7.221 + if name.size == 1 && Kind.markup.isDefinedAt(name(0)) =>
7.222 + put_result(Kind.markup(name(0)), props, body)
7.223 case _ => throw new Protocol_Error("bad header: " + header.toString)
7.224 }
7.225 }
7.226 @@ -341,15 +307,15 @@
7.227 }
7.228 catch {
7.229 case e: IOException =>
7.230 - put_result(Kind.SYSTEM, "Cannot read message:\n" + e.getMessage)
7.231 + put_result(Markup.SYSTEM, "Cannot read message:\n" + e.getMessage)
7.232 case e: Protocol_Error =>
7.233 - put_result(Kind.SYSTEM, "Malformed message:\n" + e.getMessage)
7.234 + put_result(Markup.SYSTEM, "Malformed message:\n" + e.getMessage)
7.235 }
7.236 } while (c != -1)
7.237 stream.close
7.238 try_close()
7.239
7.240 - put_result(Kind.SYSTEM, "Message thread terminated")
7.241 + put_result(Markup.SYSTEM, "Message thread terminated")
7.242 }
7.243 }
7.244
7.245 @@ -392,8 +358,8 @@
7.246 override def run() = {
7.247 val rc = proc.waitFor()
7.248 Thread.sleep(300) // FIXME property!?
7.249 - put_result(Kind.SYSTEM, "Exit thread terminated")
7.250 - put_result(Kind.EXIT, rc.toString)
7.251 + put_result(Markup.SYSTEM, "Exit thread terminated")
7.252 + put_result(Markup.EXIT, rc.toString)
7.253 rm_fifo()
7.254 }
7.255 }.start
8.1 --- a/src/Pure/System/session.scala Mon Jul 05 10:42:27 2010 +0200
8.2 +++ b/src/Pure/System/session.scala Mon Jul 05 10:47:39 2010 +0200
8.3 @@ -110,14 +110,14 @@
8.4 {
8.5 raw_results.event(result)
8.6
8.7 - val target_id: Option[Session.Entity_ID] = Position.get_id(result.props)
8.8 + val target_id: Option[Session.Entity_ID] = Position.get_id(result.message.attributes)
8.9 val target: Option[Session.Entity] =
8.10 target_id match {
8.11 case None => None
8.12 case Some(id) => lookup_entity(id)
8.13 }
8.14 if (target.isDefined) target.get.consume(result.message, indicate_command_change)
8.15 - else if (result.kind == Isabelle_Process.Kind.STATUS) {
8.16 + else if (result.is_status) {
8.17 // global status message
8.18 result.body match {
8.19
8.20 @@ -145,7 +145,7 @@
8.21 case _ => if (!result.is_ready) bad_result(result)
8.22 }
8.23 }
8.24 - else if (result.kind == Isabelle_Process.Kind.EXIT)
8.25 + else if (result.kind == Markup.EXIT)
8.26 prover = null
8.27 else if (result.is_raw)
8.28 raw_output.event(result)
8.29 @@ -176,7 +176,7 @@
8.30 {
8.31 receiveWithin(timeout) {
8.32 case result: Isabelle_Process.Result
8.33 - if result.kind == Isabelle_Process.Kind.INIT =>
8.34 + if result.kind == Markup.INIT =>
8.35 while (receive {
8.36 case result: Isabelle_Process.Result =>
8.37 handle_result(result); !result.is_ready
8.38 @@ -184,7 +184,7 @@
8.39 None
8.40
8.41 case result: Isabelle_Process.Result
8.42 - if result.kind == Isabelle_Process.Kind.EXIT =>
8.43 + if result.kind == Markup.EXIT =>
8.44 Some(startup_error())
8.45
8.46 case TIMEOUT => // FIXME clarify
9.1 --- a/src/Pure/goal.ML Mon Jul 05 10:42:27 2010 +0200
9.2 +++ b/src/Pure/goal.ML Mon Jul 05 10:47:39 2010 +0200
9.3 @@ -104,12 +104,7 @@
9.4
9.5 (* parallel proofs *)
9.6
9.7 -fun fork e = Future.fork_pri ~1 (fn () =>
9.8 - let
9.9 - val _ = Output.status (Markup.markup Markup.forked "");
9.10 - val x = e (); (*sic*)
9.11 - val _ = Output.status (Markup.markup Markup.joined "");
9.12 - in x end);
9.13 +fun fork e = Future.fork_pri ~1 (fn () => Future.report e);
9.14
9.15 val parallel_proofs = Unsynchronized.ref 1;
9.16
10.1 --- a/src/Pure/library.scala Mon Jul 05 10:42:27 2010 +0200
10.2 +++ b/src/Pure/library.scala Mon Jul 05 10:47:39 2010 +0200
10.3 @@ -129,11 +129,12 @@
10.4
10.5 def timeit[A](message: String)(e: => A) =
10.6 {
10.7 - val start = System.currentTimeMillis()
10.8 + val start = System.nanoTime()
10.9 val result = Exn.capture(e)
10.10 - val stop = System.currentTimeMillis()
10.11 + val stop = System.nanoTime()
10.12 System.err.println(
10.13 - (if (message.isEmpty) "" else message + ": ") + (stop - start) + "ms elapsed time")
10.14 + (if (message == null || message.isEmpty) "" else message + ": ") +
10.15 + ((stop - start).toDouble / 1000000) + "ms elapsed time")
10.16 Exn.release(result)
10.17 }
10.18 }
11.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala Mon Jul 05 10:42:27 2010 +0200
11.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala Mon Jul 05 10:47:39 2010 +0200
11.3 @@ -95,14 +95,6 @@
11.4 def to_current(doc: Document, offset: Int): Int =
11.5 (offset /: changes_from(doc)) ((i, change) => change after i)
11.6
11.7 - def lines_of_command(doc: Document, cmd: Command): (Int, Int) =
11.8 - {
11.9 - val start = doc.command_start(cmd).get // FIXME total?
11.10 - val stop = start + cmd.length
11.11 - (buffer.getLineOfOffset(to_current(doc, start)),
11.12 - buffer.getLineOfOffset(to_current(doc, stop)))
11.13 - }
11.14 -
11.15
11.16 /* text edits */
11.17
12.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala Mon Jul 05 10:42:27 2010 +0200
12.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala Mon Jul 05 10:47:39 2010 +0200
12.3 @@ -104,13 +104,10 @@
12.4 react {
12.5 case Command_Set(changed) =>
12.6 Swing_Thread.now {
12.7 + // FIXME cover doc states as well!!?
12.8 val document = model.recent_document()
12.9 - // FIXME cover doc states as well!!?
12.10 - for (command <- changed if document.commands.contains(command)) {
12.11 - update_syntax(document, command)
12.12 - invalidate_line(document, command)
12.13 - overview.repaint()
12.14 - }
12.15 + if (changed.exists(document.commands.contains))
12.16 + full_repaint(document, changed)
12.17 }
12.18
12.19 case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
12.20 @@ -118,34 +115,82 @@
12.21 }
12.22 }
12.23
12.24 + def full_repaint(document: Document, changed: Set[Command])
12.25 + {
12.26 + Swing_Thread.assert()
12.27 +
12.28 + val buffer = model.buffer
12.29 + var visible_change = false
12.30 +
12.31 + for ((command, start) <- document.command_starts) {
12.32 + if (changed(command)) {
12.33 + val stop = start + command.length
12.34 + val line1 = buffer.getLineOfOffset(model.to_current(document, start))
12.35 + val line2 = buffer.getLineOfOffset(model.to_current(document, stop))
12.36 + if (line2 >= text_area.getFirstLine &&
12.37 + line1 <= text_area.getFirstLine + text_area.getVisibleLines)
12.38 + visible_change = true
12.39 + text_area.invalidateLineRange(line1, line2)
12.40 + }
12.41 + }
12.42 + if (visible_change) model.buffer.propertiesChanged()
12.43 +
12.44 + overview.repaint() // FIXME paint here!?
12.45 + }
12.46 +
12.47
12.48 /* text_area_extension */
12.49
12.50 private val text_area_extension = new TextAreaExtension
12.51 {
12.52 - override def paintValidLine(gfx: Graphics2D,
12.53 - screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
12.54 + override def paintScreenLineRange(gfx: Graphics2D,
12.55 + first_line: Int, last_line: Int, physical_lines: Array[Int],
12.56 + start: Array[Int], end: Array[Int], y0: Int, line_height: Int)
12.57 {
12.58 - val document = model.recent_document()
12.59 - def from_current(pos: Int) = model.from_current(document, pos)
12.60 - def to_current(pos: Int) = model.to_current(document, pos)
12.61 + Swing_Thread.now {
12.62 + val document = model.recent_document()
12.63 + def from_current(pos: Int) = model.from_current(document, pos)
12.64 + def to_current(pos: Int) = model.to_current(document, pos)
12.65
12.66 - val line_end = model.visible_line_end(start, end)
12.67 - val line_height = text_area.getPainter.getFontMetrics.getHeight
12.68 + val command_range: Iterable[(Command, Int)] =
12.69 + {
12.70 + val range = document.command_range(from_current(start(0)))
12.71 + if (range.hasNext) {
12.72 + val (cmd0, start0) = range.next
12.73 + new Iterable[(Command, Int)] {
12.74 + def iterator = Document.command_starts(document.commands.iterator(cmd0), start0)
12.75 + }
12.76 + }
12.77 + else Iterable.empty
12.78 + }
12.79
12.80 - val saved_color = gfx.getColor
12.81 - try {
12.82 - for ((command, command_start) <-
12.83 - document.command_range(from_current(start), from_current(line_end)) if !command.is_ignored)
12.84 - {
12.85 - val p = text_area.offsetToXY(start max to_current(command_start))
12.86 - val q = text_area.offsetToXY(line_end min to_current(command_start + command.length))
12.87 - assert(p.y == q.y)
12.88 - gfx.setColor(Document_View.choose_color(document, command))
12.89 - gfx.fillRect(p.x, y, q.x - p.x, line_height)
12.90 + val saved_color = gfx.getColor
12.91 + try {
12.92 + var y = y0
12.93 + for (i <- 0 until physical_lines.length) {
12.94 + if (physical_lines(i) != -1) {
12.95 + val line_start = start(i)
12.96 + val line_end = model.visible_line_end(line_start, end(i))
12.97 +
12.98 + val a = from_current(line_start)
12.99 + val b = from_current(line_end)
12.100 + val cmds = command_range.iterator.
12.101 + dropWhile { case (cmd, c) => c + cmd.length <= a } .
12.102 + takeWhile { case (_, c) => c < b }
12.103 +
12.104 + for ((command, command_start) <- cmds if !command.is_ignored) {
12.105 + val p = text_area.offsetToXY(line_start max to_current(command_start))
12.106 + val q = text_area.offsetToXY(line_end min to_current(command_start + command.length))
12.107 + assert(p.y == q.y)
12.108 + gfx.setColor(Document_View.choose_color(document, command))
12.109 + gfx.fillRect(p.x, y, q.x - p.x, line_height)
12.110 + }
12.111 + }
12.112 + y += line_height
12.113 + }
12.114 }
12.115 + finally { gfx.setColor(saved_color) }
12.116 }
12.117 - finally { gfx.setColor(saved_color) }
12.118 }
12.119
12.120 override def getToolTipText(x: Int, y: Int): String =
12.121 @@ -186,30 +231,6 @@
12.122 }
12.123
12.124
12.125 - /* (re)painting */
12.126 -
12.127 - private val update_delay = Swing_Thread.delay_first(500) { model.buffer.propertiesChanged() }
12.128 - // FIXME update_delay property
12.129 -
12.130 - private def update_syntax(document: Document, cmd: Command)
12.131 - {
12.132 - val (line1, line2) = model.lines_of_command(document, cmd)
12.133 - if (line2 >= text_area.getFirstLine &&
12.134 - line1 <= text_area.getFirstLine + text_area.getVisibleLines)
12.135 - update_delay()
12.136 - }
12.137 -
12.138 - private def invalidate_line(document: Document, cmd: Command) =
12.139 - {
12.140 - val (start, stop) = model.lines_of_command(document, cmd)
12.141 - text_area.invalidateLineRange(start, stop)
12.142 - }
12.143 -
12.144 - private def invalidate_all() =
12.145 - text_area.invalidateLineRange(text_area.getFirstPhysicalLine,
12.146 - text_area.getLastPhysicalLine)
12.147 -
12.148 -
12.149 /* overview of command status left of scrollbar */
12.150
12.151 private val overview = new JPanel(new BorderLayout)
12.152 @@ -252,9 +273,9 @@
12.153 val buffer = model.buffer
12.154 val document = model.recent_document()
12.155 def to_current(pos: Int) = model.to_current(document, pos)
12.156 - val saved_color = gfx.getColor
12.157 + val saved_color = gfx.getColor // FIXME needed!?
12.158 try {
12.159 - for ((command, start) <- document.command_range(0) if !command.is_ignored) {
12.160 + for ((command, start) <- document.command_starts if !command.is_ignored) {
12.161 val line1 = buffer.getLineOfOffset(to_current(start))
12.162 val line2 = buffer.getLineOfOffset(to_current(start + command.length)) + 1
12.163 val y = line_to_y(line1)